git.iko.soy/Idris-dev
on cd58dfb help sign in
Idris-dev/test/error004/expected
20 lines 542 B history raw
1FunErrTest.idr:35:12-18:
2 |
335 | badCadr1 = cadr []
4 | ~~~~~~~
5When checking right hand side of badCadr1 with expected type
6 Int
8When checking argument cons2 to function FunErrTest.cadr:
9 Could not prove that [] has at least two elements.
11FunErrTest.idr:38:12-19:
12 |
1338 | badCadr2 = cadr [1]
14 | ~~~~~~~~
15When checking right hand side of badCadr2 with expected type
16 Int
18When checking argument cons2 to function FunErrTest.cadr:
19 Could not prove that [] has at least two elements.