1a86305 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make believe_me abstract

commit1a8630578c2e3af7881b4cdf19987ed9bd7f737b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 13 Nov 2012, 12:06 (14 years ago) parent718a040

2 files changed+2−1

unifiedsplit

lib/Builtins.idr+1

@@ -31,6 +31,7 @@ malloc size x = x -- compiled specially

3131trace_malloc : a -> a

3232trace_malloc x = x -- compiled specially

3333

34+abstract

3435believe_me : a -> b -- compiled specially as id, use with care!

3536believe_me x = prim__believe_me _ _ x

3637

src/Idris/Delaborate.hs+1−1

@@ -85,7 +85,7 @@ pshow i (CantUnify _ x y e sc s)

8585 _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++

8686 if (opt_errContext (idris_options i)) then showSc i sc else ""

8787pshow i (CantConvert x y env)

88− = "Can't unify " ++ show (delab i x) ++ " with " ++ show (delab i y) ++

88+ = "Can't convert " ++ show (delab i x) ++ " with " ++ show (delab i y) ++

8989 if (opt_errContext (idris_options i)) then showSc i env else ""

9090pshow i (InfiniteUnify x tm env)

9191 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++