search

sbp / idris-bi

Idris Binary Integer Arithmetic, porting PArith, NArith, and ZArith from Coq
https://github.com/idris-lang/Idris-dev/issues/3976
36 stars 5 forks source link

Bip comparison proofs #4

Closed clayrat closed 7 years ago

clayrat commented 7 years ago

These start to feel a bit clunky, maybe Idris should have some sugar for the 

rewrite foo in aux
where
aux : Bar 
aux with (...)

pattern.

sbp commented 7 years ago

I get type checking errors in Data.Bip.Proofs.ltbLtTo and Data.Bip.Proofs.lebLeTo. Here's the first of those, and the second is similar:

./Data/Bip/Proofs.idr:817:8:
When checking right hand side of with block in Data.Bip.Proofs.ltbLtTo with expected type
        EQ = LT

Can't find implementation for Uninhabited (with block in Prelude.Interfaces.Data.Bip.Bip 
    implementation of Prelude.Interfaces.Ord, method < EQ
                                                       p
                                                       q =
                                           True)

I tried to fix this, but couldn't work out how. Any ideas?

clayrat commented 7 years ago

Hm, prf in that block should reduce to False = True. What version of Idris are you on? I think the Uninhabited instances for Bool were added in 1.1.0.

clayrat commented 7 years ago

If you don't want to upgrade for the moment, try adding these somewhere in the file locally:

Uninhabited (True = False) where
  uninhabited Refl impossible

Uninhabited (False = True) where
  uninhabited Refl impossible
sbp commented 7 years ago

Oops, I was indeed on 1.0. Thanks!