git.iko.soy/Idris-dev
on master help sign in
Fix integer literals at REPL
commit13b182f1324c99122ac73fbab9c43c1337ca1893 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 18 Nov 2013, 15:30 (13 years ago) parentb37d0f4
3 files changed+4−6
compare with master
unifiedsplit
src/Idris/ElabDecls.hs+2−3 test/test032/expected+1−2 test/test032/input+1−1
src/Idris/ElabDecls.hs+2−3
@@ -843,8 +843,7 @@ elabValBind :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])
843843elabValBind info aspat tm_in
844844 = do ctxt <- getContext
845845 i <- getIState
846− let tm = if aspat then addImplPat i tm_in
847− else addImpl i tm_in
846+ let tm = addImpl i tm_in
848847 logLvl 10 (showImp Nothing True False tm)
849848 -- try:
850849 -- * ordinary elaboration
@@ -855,7 +854,7 @@ elabValBind info aspat tm_in
855854-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
856855-- (build i info aspat (MN 0 "val") tm))
857856 tclift (elaborate ctxt (MN 0 "val") infP []
858− (buildTC i info aspat False (MN 0 "val") (infTerm tm)))
857+ (build i info aspat (MN 0 "val") (infTerm tm)))
859858 let vtm = orderPats (getInferTerm tm')
860859
861860 def' <- checkDef (fileFC "(input)") defer
test/test032/expected+1−2
@@ -2,8 +2,7 @@ Type checking ./test032.idr
22isElem x [] = ?isElem_rhs_1
33isElem x (_ :: _) = ?isElem_rhs_3
44
5− localZipWith f (_ :: _) ys = ?localZipWith_rhs_1
6− localZipWith f (_ :: _) ys = ?localZipWith_rhs_2
5+ localZipWith f (_ :: _) (_ :: _) = ?localZipWith_rhs_1
76
87f x :: (map f xs)
98isElem2 x (y :: ys) with (_)
test/test032/input+1−1
@@ -1,5 +1,5 @@
11:cs 11 xs
2−:cs 17 xs
2+:cs 17 ys
33:ps 21 maprhs
44:mw 25 isElem2
55:cs 30 p