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

Duplication of binDouble/binDoubleSucc #16

Open clayrat opened 7 years ago

clayrat commented 7 years ago

We seem to have two versions of those: in Bip, to define bipAnd/bipDiff/bipXor, and in Bin proper as binDPO/binD. As we don't have any proofs of bipAnd etc in Bip, might as well move those to Bin to avoid duplication?

clayrat commented 7 years ago

This will also help to do https://github.com/sbp/idris-bi/issues/8 as the functions mentioned reference Bin.