Refactor, add more proofs

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

Refactor, add more proofs #1

Closed clayrat closed 7 years ago

clayrat commented 7 years ago

Minor edits in README.md
Added a folder structure
Split proofs into pattern-matching and Pruviloj parts to speed up typechecking
Added more proofs to Data.Bip.Proofs

clayrat commented 7 years ago

One thing I should mention is that one-line proofs with Refl (e.g., iSuccO, predDoubleSpec, etc) are pretty much useless in Idris, as it will eagerly simplify such expressions in-place. This means you can't use them to "de-normalize" the expression in the other way.

sbp commented 7 years ago

This is great, thanks so much! Data.Bip.Proofs.mulComm needs to be covering, and the Makefile needs updating but I'll fix those things in a subsequent followup commit.

Since the goal is to have this merged into Idris, I assume you're okay with the Idris license?

https://github.com/idris-lang/Idris-dev/blob/master/LICENSE

Can you signify here that you're explicitly okay with that for your contributions? Then I can add a LICENSE file too.

clayrat commented 7 years ago

Yeah the license seems ok, I've already contributed to Idris in the past anyway :)