Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtil | 2018-08-23 | |
* | Make Z.div_mod_to_quot_rem stronger | 2018-07-10 | |
* | Add MontgomeryAPI.encode and two lemmas about it | 2017-11-14 | |
* | Add more versions of basesystem_partial_evaluation_unfolder | 2017-11-07 | |
* | Fix bug in previous commit | 2017-10-20 | |
* | Switch arithmetic to cps for Z * Z under the hood | 2017-10-19 | |
* | More fine-grained tactics imports | 2017-07-08 | |
* | Remove some admitted lemmas | 2017-07-07 | |
* | Closed under the global context | 2017-07-02 | |
* | prove [MontgomeryAPI.small_add] | 2017-07-02 | |
* | [small] admits progress... | 2017-07-01 | |
* | change opp to runtime_opp | 2017-07-01 | |
* | proved remaining [eval] admits in MontgomeryAPI | 2017-07-01 | |
* | Prove saturated carrying-addition-chain correct | 2017-06-30 | |
* | Reorganization of saturated arithmetic | 2017-06-29 |