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