Revert "temporarily updating the error messages for error001 and error004. they need to be looked at."
This reverts commit 3a0f464f5c068db062501de1244604f1e0a73e04.
commit1df37d2fb457cc53217a538a09989b311d139c07
authorOzgur Akgun <ozgurakgun@gmail.com>
dateFri 20 Mar 2015, 14:15 (12 years ago)
parent3a0f464
test/error001/expected+1−10
@@ -1,10 +1 @@
1−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−
1+test002.idr:5:6:Universe inconsistency
test/error004/expected+2−4
@@ -1,8 +1,6 @@
11FunErrTest.idr:35:10:When elaborating right hand side of badCadr1:
22When elaborating argument cons1 to function FunErrTest.cadr:
3− Can't solve goal
4− isCons [] = True
3+ Could not prove that [] has at least two elements.
54FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:
65When 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.