Make test038 actually test something
commit3705a6bb1dbc4dcd91eae82fb1c526fc304dc9b4
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateFri 24 Jan 2014, 19:52 (13 years ago)
parent7c39186
test/test038/FunErrTest.idr+8
@@ -31,3 +31,11 @@ has2elts e = Just [TextPart (show e)]
3131%error_handlers cadr cons1 has2elts
3232%error_handlers cadr cons2 has2elts
3333
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.