@@ -100,6 +100,12 @@ getGuess = prim__Guess
100100lookupTy : TTName -> Elab (List (TTName, NameType, TT))
101101lookupTy n = prim__LookupTy n
102102
103+lookupTyExact : TTName -> Elab (TTName, NameType, TT)
104+lookupTyExact n = case !(lookupTy n) of
105+ [res] => return res
106+ [] => fail [NamePart n, TextPart "is not defined."]
107+ xs => fail [NamePart n, TextPart "is ambiguous."]
108+
103109forgetTypes : TT -> Elab Raw
104110forgetTypes tt = prim__Forget tt
105111