git.iko.soy/Idris-dev
on master help sign in
Revert "temporarily updating the error messages for error001 and error004. they need to be looked at."
1df37d2Ozgur Akgun
test/error001/expected+1−10
compare with master
unifiedsplit
@@ -1,10 +1 @@
1−Universe inconsistency.
1+test002.idr:5:6:Universe inconsistency
2−Working on: v2
3−Old domain: Domain 7 7
4−New domain: Domain 7 6
5−Involved constraints:
6− (v2 <= s1,test002.idr:5:6)
7− (u2 < v2,test002.idr:5:6)
8− (t1 <= v2,test002.idr:5:6)
9− (v2 <= s1,test002.idr:5:6)
10−
test/error004/expected+2−4
@@ -1,8 +1,6 @@
1FunErrTest.idr:35:10:When elaborating right hand side of badCadr1:
1FunErrTest.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− Can't solve goal
3+ Could not prove that [] has at least two elements.
4− isCons [] = True
5FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:
4FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:
6When elaborating argument cons2 to function FunErrTest.cadr:
5When elaborating argument cons2 to function FunErrTest.cadr:
7− Can't solve goal
8− isCons (tail [(fromInteger 1)]) = True
6+ Could not prove that tail [(fromInteger 1)] has at least two elements.