aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic
Commit message (Expand)AuthorAge
* 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
* create directory for saturated arithmetic in preparation for splitting into m...Gravatar jadep2017-06-29
* Merge branch 'addsubchains'Gravatar jadep2017-06-29
|\
* | new add/carry chain logic with admitted proofsGravatar jadep2017-06-29
* | Skeleton for add/subtract chains (see #222)Gravatar jadep2017-06-29
| * Fix the sense of op_{get,with}_carry in SaturatedGravatar Jason Gross2017-06-29
| * Adapt to new arguments of saturated thingsGravatar Jason Gross2017-06-29
| * Fix type signatures of saturated things for WBWGravatar Jason Gross2017-06-29
| * new add/carry chain logic with admitted proofsGravatar jadep2017-06-29
| * Skeleton for add/subtract chains (see #222)Gravatar jadep2017-06-28
|/
* proved eval_mod and eval_div (last remaining eval_ admits in Saturated)Gravatar jadep2017-06-27
* Add a comment for nonzero_cpsGravatar Jason Gross2017-06-26
* Fix a broken proofGravatar Jason Gross2017-06-26
* Factor out admitted proof into admitted lemmaGravatar Jason Gross2017-06-26
* Add nonzero synthesisGravatar Jason Gross2017-06-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 04:58:32 +0000