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

Order of multiplication in the divMod-style proofs #23

Closed clayrat closed 7 years ago

clayrat commented 7 years ago

In some places it's b*q+r, in others it's q*b+r; would be nice to choose a single style (personally I like q*b+r more) to avoid extra mulComms.