git.iko.soy/Idris-dev
on de2011f help sign in
Idris-dev/test/error005/expected
12 lines 688 B history raw
1error005.idr:13:1:When elaborating right hand side of two:
2When elaborating argument prf to function Data.Fin.fromInteger:
3 When using 2 as a literal for a Fin 2
4 Could not show that 2 is less than 2
5error005.idr:16:1:When elaborating right hand side of hahaha:
6When elaborating argument prf to function Data.Fin.fromInteger:
7 When using 0 as a literal for a Fin n
8 Could not show that 0 is less than n
9error005.idr:21:1:When elaborating right hand side of notOk:
10When elaborating argument prf to function Data.Fin.fromInteger:
11 When using 2 as a literal for a Fin (S (S n))
12 Could not show that 2 is less than S (S n)