git.iko.soy/Idris-dev
on master help sign in
REPL shouldn't try to be too clever...
d1813c9Edwin Brady
lib/Builtins.idr+1−1
compare with master
unifiedsplit
@@ -43,7 +43,7 @@ namespace Builtins {
43id : a -> a
43id : a -> a
44id x = x
44id x = x
45
45
46−the : (A : Type) -> A -> A
46+the : (a : Type) -> a -> a
47the _ = id
47the _ = id
48
48
49const : a -> b -> a
49const : a -> b -> a
src/Idris/ElabDecls.hs+3−3
@@ -462,9 +462,9 @@ elabVal info aspat tm_in
462 -- * elaboration as a function a -> b
462 -- * elaboration as a function a -> b
463
463
464 ((tm', defer, is), _) <-
464 ((tm', defer, is), _) <-
465− tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
465+-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
466− (build i info aspat (MN 0 "val") tm))
466+-- (build i info aspat (MN 0 "val") tm))
467− (elaborate ctxt (MN 0 "val") infP []
467+ tclift (elaborate ctxt (MN 0 "val") infP []
468 (build i info aspat (MN 0 "val") (infTerm tm)))
468 (build i info aspat (MN 0 "val") (infTerm tm)))
469 logLvl 3 ("Value: " ++ show tm')
469 logLvl 3 ("Value: " ++ show tm')
470 recheckC (FC "(input)" 0) [] tm'
470 recheckC (FC "(input)" 0) [] tm'