idris-0.9.16: test/error005/expected
error005.idr:13:1:When elaborating right hand side of two:
When elaborating argument prf to function Data.Fin.fromInteger:
When using 2 as a literal for a Fin 2
Could not show that 2 is less than 2
error005.idr:16:1:When elaborating right hand side of hahaha:
When elaborating argument prf to function Data.Fin.fromInteger:
When using 0 as a literal for a Fin n
Could not show that 0 is less than n
error005.idr:21:1:When elaborating right hand side of notOk:
When elaborating argument prf to function Data.Fin.fromInteger:
When using 2 as a literal for a Fin (S (S n))
Could not show that 2 is less than S (S n)