packages feed

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)