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