aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/Core.v
Commit message (Expand)AuthorAge
* update _CoqProject, fix indentations, and prune dependencies of new Arithmeti...Gravatar jadep2019-04-03
* split up Arithmetic (imports etc. not yet fixed, does not build)Gravatar jadep2019-04-03
* remove old pipelineGravatar Andres Erbsen2019-01-09
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Move chained_carries' (now chained_carries_reduce)Gravatar 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
* Use fold_right_cps2 to get eqb_cps to get the right continuation typeGravatar Jason Gross2017-10-19
* Switch arithmetic to cps for Z * Z under the hoodGravatar 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
* 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 cbv_runtime in Arithmetic/CoreGravatar Jason Gross2017-07-08
* Add nonzero synthesisGravatar Jason Gross2017-06-26
* define strong small and re-prove small_add and small_compact with that defini...Gravatar jadep2017-06-18
* Improve replace_match_with_destructuring_matchGravatar Jason Gross2017-06-15
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* export a few more wrapper definitions in PositionalGravatar jadep2017-06-02
* Strip trailing whitespaceGravatar Jason Gross2017-06-02
* force carry intermediates to be bound earlyGravatar Andres Erbsen2017-05-14
* make freeze use the correct versions of add_get_carry and zselectGravatar jadep2017-05-14
* move some lemmas to Core and define a tuple-select operationGravatar jadep2017-05-01
* stricter divmod proofsGravatar jadep2017-05-01
* rename-everythingGravatar Andres Erbsen2017-04-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-12 00:17:31 +0000