git.iko.soy/Idris-dev
on 313340e help sign in
Idris-dev/test/error004/expected
6 lines 399 B history raw
1FunErrTest.idr:35:10:When elaborating right hand side of badCadr1:
2When elaborating argument cons1 to function FunErrTest.cadr:
3 Could not prove that [] has at least two elements.
4FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:
5When elaborating argument cons2 to function FunErrTest.cadr:
6 Could not prove that tail [(fromInteger 1)] refl has at least two elements.