git.iko.soy/Idris-dev
on f0a67ff help sign in
Idris-dev/test/error005/expected
36 lines 1.3 kB history raw
1error005.idr:13:1:
2When checking right hand side of two with expected type
3 Fin 2
5When checking argument prf to function Data.Fin.fromInteger:
6 When using 2 as a literal for a Fin 2
7 2 is not strictly less than 2
8error005.idr:16:1:
9When checking right hand side of hahaha with expected type
10 Fin n
12When checking argument prf to function Data.Fin.fromInteger:
13 When using 0 as a literal for a Fin n
14 0 is not strictly less than n
15error005.idr:22:1:
16When checking right hand side of notOk with expected type
17 Fin (plus 2 n)
19When checking argument prf to function Data.Fin.fromInteger:
20 When using 2 as a literal for a Fin (S (S n))
21 2 is not strictly less than S (S n)
22error005.idr:23:24:
23When checking right hand side of b0rken with expected type
24 Fin 3
26When checking argument prf to function Data.Fin.fromInteger:
27 When using n as a literal for a Fin 3
28 Could not show that n is less than 3 because n is a bound
29 variable instead of a constant Integer
30error005.idr:28:1:
31When checking right hand side of x with expected type
32 Fin 4
34When checking argument prf to function Data.Fin.fromInteger:
35 When using 5 as a literal for a Fin 4
36 5 is not strictly less than 4