git.iko.soy/Idris-dev
on master help sign in
Fix test
f490d9fDavid Raymond Christiansen
test/error004/expected+2−2
compare with master
unifiedsplit
@@ -1,6 +1,6 @@
1−FunErrTest.idr:33:10:When elaborating right hand side of badCadr1:
1+FunErrTest.idr:35:10:When elaborating right hand side of badCadr1:
2When elaborating argument cons1 to function FunErrTest.cadr:
2When elaborating argument cons1 to function FunErrTest.cadr:
3 Could not prove that [] has at least two elements.
3 Could not prove that [] has at least two elements.
4−FunErrTest.idr:36:10:When elaborating right hand side of badCadr2:
4+FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:
5When elaborating argument cons2 to function FunErrTest.cadr:
5When elaborating argument cons2 to function FunErrTest.cadr:
6 Could not prove that tail [(fromInteger 1)] refl has at least two elements.
6 Could not prove that tail [(fromInteger 1)] refl has at least two elements.