13b182f · Idris-dev · git.iko.soy

src/Idris/ElabDecls.hs+2−3

compare with master

unifiedsplit

@@ -843,8 +843,7 @@ elabValBind :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])

843elabValBind info aspat tm_in

844 = do ctxt <- getContext

845 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

848 logLvl 10 (showImp Nothing True False tm)

847 logLvl 10 (showImp Nothing True False tm)

849 -- try:

848 -- try:

850 -- * ordinary elaboration

849 -- * ordinary elaboration

@@ -855,7 +854,7 @@ elabValBind info aspat tm_in

855-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []

854-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []

856-- (build i info aspat (MN 0 "val") tm))

855-- (build i info aspat (MN 0 "val") tm))

857 tclift (elaborate ctxt (MN 0 "val") infP []

856 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)))

859 let vtm = orderPats (getInferTerm tm')

858 let vtm = orderPats (getInferTerm tm')

860

859

861 def' <- checkDef (fileFC "(input)") defer

860 def' <- checkDef (fileFC "(input)") defer

test/test032/expected+1−2

@@ -2,8 +2,7 @@ Type checking ./test032.idr

2isElem x [] = ?isElem_rhs_1

3isElem x (_ :: _) = ?isElem_rhs_3

4

5− localZipWith f (_ :: _) ys = ?localZipWith_rhs_1

5+ localZipWith f (_ :: _) (_ :: _) = ?localZipWith_rhs_1

6− localZipWith f (_ :: _) ys = ?localZipWith_rhs_2

7

6

8f x :: (map f xs)

7f x :: (map f xs)

9isElem2 x (y :: ys) with (_)

8isElem2 x (y :: ys) with (_)

test/test032/input+1−1

@@ -1,5 +1,5 @@

1:cs 11 xs

2−:cs 17 xs

2+:cs 17 ys

3:ps 21 maprhs

4:mw 25 isElem2

5:cs 30 p