git.iko.soy/Idris-dev
on master help sign in
temporarily updating the error messages for error001 and error004. they need to be looked at.
3a0f464Ozgur Akgun
test/error001/expected+10−1
compare with master
unifiedsplit
@@ -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 @@
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− Could not prove that [] has at least two elements.
3+ Can't solve goal
4+ isCons [] = True
4FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:
5FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:
5When elaborating argument cons2 to function FunErrTest.cadr:
6When elaborating argument cons2 to function FunErrTest.cadr:
7+ Can't solve goal
6− Could not prove that tail [(fromInteger 1)] has at least two elements.
8+ isCons (tail [(fromInteger 1)]) = True