git.iko.soy/Idris-dev
on master help sign in
Make test038 actually test something
3705a6bDavid Raymond Christiansen
test/test038/FunErrTest.idr+8
compare with master
unifiedsplit
@@ -31,3 +31,11 @@ has2elts e = Just [TextPart (show e)]
31%error_handlers cadr cons1 has2elts
31%error_handlers cadr cons1 has2elts
32%error_handlers cadr cons2 has2elts
32%error_handlers cadr cons2 has2elts
33
33
34+badCadr1 : Int
35+badCadr1 = cadr []
36+
37+badCadr2 : Int
38+badCadr2 = cadr [1]
39+
40+goodCadr : Int
41+goodCadr = cadr [1, 2]
test/test038/expected+4
@@ -0,0 +1,4 @@
1+FunErrTest.idr:35:10:When elaborating right hand side of badCadr1:
2+Could not prove that [] has at least two elements.
3+FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:
4+Could not prove that Prelude.List.tail [(Prelude.Classes.fromInteger 1)] refl has at least two elements.