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