aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic
Commit message (Expand)AuthorAge
* 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 karatsuba, goldilocks lemmas to rewrite dbsGravatar Jason Gross2017-11-07
* Move chained_carries' (now chained_carries_reduce)Gravatar Jason Gross2017-11-07
* Add more versions of basesystem_partial_evaluation_unfolderGravatar Jason Gross2017-11-07
* Split off computational part of basesystem_partial_evaluation_RHS_genGravatar Jason Gross2017-11-07
* More use of Z.eqb_cpsGravatar Jason Gross2017-11-07
* Use div_cps and modulo_cps in more placesGravatar Jason Gross2017-11-07
* Make use of id_tuple_with_alt_cps'Gravatar Jason Gross2017-11-06
* Make use of from_associational_cps in more placesGravatar Jason Gross2017-11-01
* More use of Z.eqb_cpsGravatar Jason Gross2017-11-01
* 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
* Move tactics around in src/Arithmetic/CoreUnfolder.vGravatar Jason Gross2017-10-19
* Pattern over cps lemmas in Arithmetic/CoreGravatar Jason Gross2017-10-19
* Unfold more things in basesystem_partial_evaluation_unfolderGravatar Jason Gross2017-10-18
* Add some more things to basesystem_partial_evaluation_unfolderGravatar Jason Gross2017-10-18
* Add basesystem_partial_evaluation_unfolder dbGravatar Jason Gross2017-10-18
* Unfold more things in core unfolderGravatar Jason Gross2017-10-18
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-18
* Pattern more things in arithmetic/coreGravatar Jason Gross2017-10-17
* Add MulSplitUnfolderGravatar Jason Gross2017-10-17
* Add faster arithmetic unfoldingGravatar Jason Gross2017-10-15
* Extend basesystem_partial_evaluation_RHSGravatar Jason Gross2017-10-15
* Fix a typo in the previous commitGravatar Jason Gross2017-10-14
* Split up solve_op_mod_eqGravatar Jason Gross2017-10-14
* Add UniformWeightInstancesGravatar Jason Gross2017-10-09
* Add cbv_runtime in Arithmetic/CoreGravatar Jason Gross2017-07-08
* More fine-grained tactics importsGravatar Jason Gross2017-07-08
* Remove some admitted lemmasGravatar Jason Gross2017-07-07
* enforce use of [F.zero], [F.one]; prove Ed25519 admitsGravatar Andres Erbsen2017-07-07
* prove ModularArithmeticTheorems admitsGravatar Andres Erbsen2017-07-06
* Fix a typo that ends up not matteringGravatar Jason Gross2017-07-06
* Closed under the global contextGravatar Andres Erbsen2017-07-02
* prove [MontgomeryAPI.small_add]Gravatar Andres Erbsen2017-07-02
* fix [small_div] argumentsGravatar 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 16:33:10 +0000