error005.idr:13:1:When checking right hand side of two: When checking argument prf to function Data.Fin.fromInteger: When using 2 as a literal for a Fin 2 2 is not strictly less than 2 error005.idr:16:1:When checking right hand side of hahaha: When checking argument prf to function Data.Fin.fromInteger: When using 0 as a literal for a Fin n 0 is not strictly less than n error005.idr:22:1:When checking right hand side of notOk: When checking argument prf to function Data.Fin.fromInteger: When using 2 as a literal for a Fin (S (S n)) 2 is not strictly less than S (S n) error005.idr:23:24:When checking right hand side of b0rken: When checking argument prf to function Data.Fin.fromInteger: When using n as a literal for a Fin 3 Could not show that n is less than 3 because n is a bound variable instead of a constant Integer error005.idr:28:1:When checking right hand side of x: When checking argument prf to function Data.Fin.fromInteger: When using 5 as a literal for a Fin 4 5 is not strictly less than 4