git.iko.soy/Idris-dev
on master help sign in
REPL shouldn't try to be too clever...

Fixes first part of issue #150

commitd1813c9c3ef5ed6eb858b53288f8e73fd42ca646 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 11 Jan 2013, 19:29 (14 years ago) parent265d9a4
2 files changed+4−4
compare with master
unifiedsplit
lib/Builtins.idr+1−1 src/Idris/ElabDecls.hs+3−3
lib/Builtins.idr+1−1
@@ -43,7 +43,7 @@ namespace Builtins {
4343id : a -> a
4444id x = x
4545
46−the : (A : Type) -> A -> A
46+the : (a : Type) -> a -> a
4747the _ = id
4848
4949const : a -> b -> a
src/Idris/ElabDecls.hs+3−3
@@ -462,9 +462,9 @@ elabVal info aspat tm_in
462462 -- * elaboration as a function a -> b
463463
464464 ((tm', defer, is), _) <-
465− tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
466− (build i info aspat (MN 0 "val") tm))
467− (elaborate ctxt (MN 0 "val") infP []
465+-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
466+-- (build i info aspat (MN 0 "val") tm))
467+ tclift (elaborate ctxt (MN 0 "val") infP []
468468 (build i info aspat (MN 0 "val") (infTerm tm)))
469469 logLvl 3 ("Value: " ++ show tm')
470470 recheckC (FC "(input)" 0) [] tm'