Biz proofs - Githubissues

sbp / idris-bi

Idris Binary Integer Arithmetic, porting PArith, NArith, and ZArith from Coq

36 stars 5 forks source link

Closed clayrat closed 7 years ago

clayrat commented 7 years ago

constructor properties, DecEq and Neg instances
fixes for bizPlus, bizCompare, bizSquare, bizLog2, bizDiff and fromIntegerBiz
proofs!

clayrat commented 7 years ago

Finished basic proofs + conversions