aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/Saturated
Commit message (Expand)AuthorAge
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Make Z.div_mod_to_quot_rem strongerGravatar Jason Gross2018-07-10
* Fix naming issueGravatar Jade Philipoom2018-02-23
* Add MontgomeryAPI.encode and two lemmas about itGravatar Jason Gross2017-11-14
* fix commentGravatar jadep2017-11-12
* Fix another side condition issueGravatar Jason Gross2017-11-08
* Fix a bug in previous commitGravatar Jason Gross2017-11-08
* Add freeze rewrite lemmas to dbsGravatar Jason Gross2017-11-08
* Add more versions of basesystem_partial_evaluation_unfolderGravatar Jason Gross2017-11-07
* Add another unfolding databaseGravatar Jason Gross2017-10-22
* Fix bug in previous commitGravatar Jason Gross2017-10-20
* Use div_cps, modulo_cpsGravatar Jason Gross2017-10-20
* Use fold_right_cps2 to get eqb_cps to get the right continuation typeGravatar Jason Gross2017-10-19
* Add more unfolds to basesystem_partial_evaluation_unfolderGravatar Jason Gross2017-10-19
* Switch arithmetic to cps for Z * Z under the hoodGravatar Jason Gross2017-10-19
* Add basesystem_partial_evaluation_unfolder dbGravatar Jason Gross2017-10-18
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-18
* Add MulSplitUnfolderGravatar Jason Gross2017-10-17
* Add faster arithmetic unfoldingGravatar Jason Gross2017-10-15
* Extend basesystem_partial_evaluation_RHSGravatar Jason Gross2017-10-15
* Add UniformWeightInstancesGravatar Jason Gross2017-10-09
* More fine-grained tactics importsGravatar Jason Gross2017-07-08
* Remove some admitted lemmasGravatar Jason Gross2017-07-07
* Closed under the global contextGravatar Andres Erbsen2017-07-02
* prove [MontgomeryAPI.small_add]Gravatar Andres Erbsen2017-07-02
* [small] admits progress...Gravatar Andres Erbsen2017-07-01
* proved small_sat_addGravatar jadep2017-07-01
* change opp to runtime_oppGravatar jadep2017-07-01
* proved remaining [eval] admits in MontgomeryAPIGravatar jadep2017-07-01
* Prove saturated carrying-subtraction-chain correctGravatar jadep2017-07-01
* Prove saturated carrying-addition-chain correctGravatar jadep2017-06-30
* Reorganization of saturated arithmeticGravatar jadep2017-06-29
* create directory for saturated arithmetic in preparation for splitting into m...Gravatar jadep2017-06-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 18:02:38 +0000