git.iko.soy/Idris-dev
on master help sign in
Reflected elab: lookup exact names
0c047fdDavid Raymond Christiansen
libs/prelude/Language/Reflection/Elab.idr+6
compare with master
unifiedsplit
@@ -100,6 +100,12 @@ getGuess = prim__Guess
100lookupTy : TTName -> Elab (List (TTName, NameType, TT))
100lookupTy : TTName -> Elab (List (TTName, NameType, TT))
101lookupTy n = prim__LookupTy n
101lookupTy n = prim__LookupTy n
102
102
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+
103forgetTypes : TT -> Elab Raw
109forgetTypes : TT -> Elab Raw
104forgetTypes tt = prim__Forget tt
110forgetTypes tt = prim__Forget tt
105
111