git.iko.soy/Idris-dev
on bd2fa8d help sign in
Idris-dev/test/error005/expected
56 lines 1.6 kB history raw
1error005.idr:11:7:
2 |
311 | two = 2
4 | ^
5When checking right hand side of two with expected type
6 Fin 2
8When checking argument prf to function Data.Fin.fromInteger:
9 When using 2 as a literal for a Fin 2
10 2 is not strictly less than 2
12error005.idr:14:12:
13 |
1414 | hahaha n = 0
15 | ^
16When checking right hand side of hahaha with expected type
17 Fin n
19When checking argument prf to function Data.Fin.fromInteger:
20 When using 0 as a literal for a Fin n
21 0 is not strictly less than n
23error005.idr:20:11:
24 |
2520 | notOk n = 2
26 | ^
27When checking right hand side of notOk with expected type
28 Fin (plus 2 n)
30When checking argument prf to function Data.Fin.fromInteger:
31 When using 2 as a literal for a Fin (S (S n))
32 2 is not strictly less than S (S n)
34error005.idr:23:12-24:
35 |
3623 | b0rken n = fromInteger n
37 | ~~~~~~~~~~~~~
38When checking right hand side of b0rken with expected type
39 Fin 3
41When checking argument prf to function Data.Fin.fromInteger:
42 When using n as a literal for a Fin 3
43 Could not show that n is less than 3 because n is a bound
44 variable instead of a constant Integer
46error005.idr:26:17:
47 |
4826 | x = the (Fin 4) 5
49 | ^
50When checking right hand side of x with expected type
51 Fin 4
53When checking argument prf to function Data.Fin.fromInteger:
54 When using 5 as a literal for a Fin 4
55 5 is not strictly less than 4