aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* pass-through after Andres's review in #334Gravatar Jade Philipoom2018-04-03
* move requires to the top of the fileGravatar Jade Philipoom2018-04-03
* make montgomery not depend on intermediate weight for multiplication being th...Gravatar Jade Philipoom2018-04-03
* rename w_half to w_mulGravatar Jade Philipoom2018-04-03
* make a more general kind of mul_converted_halve that produces the correct car...Gravatar Jade Philipoom2018-04-03
* move some lemmas to ZUtil/ListUtilGravatar Jade Philipoom2018-04-03
* move some shared lemmas between Columns/Rows into a Saturated moduleGravatar Jade Philipoom2018-04-03
* reprint Montgomery output (order of additions in Rows.flatten changed)Gravatar Jade Philipoom2018-04-03
* more proof automation in RowsGravatar Jade Philipoom2018-04-03
* automate some Rows proofsGravatar Jade Philipoom2018-04-03
* organize Rows into sectionsGravatar Jade Philipoom2018-04-03
* organize proofs into sectionsGravatar Jade Philipoom2018-04-03
* more cleanup of flatten proofsGravatar Jade Philipoom2018-04-03
* clean up some [flatten] proofsGravatar Jade Philipoom2018-04-03
* move some lemmas/hints to ListUtilGravatar Jade Philipoom2018-04-03
* fix typo and add booleans for carriesGravatar Jade Philipoom2018-04-03
* changing Montgomery notationsGravatar Jade Philipoom2018-04-03
* make add_with_get_carry with a constant zero for the carry translate to add_g...Gravatar Jade Philipoom2018-04-03
* inline shifts for Montgomery exampleGravatar Jade Philipoom2018-04-03
* Make Montgomery example use row-wise flatten (involves adding Nat.max, List.t...Gravatar Jade Philipoom2018-04-03
* add Rows.from_associational and some more length proofs that allow Rows.lengt...Gravatar Jade Philipoom2018-04-03
* move mul_converted to its own moduleGravatar Jade Philipoom2018-04-03
* finish flatten_partitions and slightly change the format of _partitions lemma...Gravatar Jade Philipoom2018-04-03
* proved admits about sum_rowsGravatar Jade Philipoom2018-04-03
* finish from_columns proofsGravatar Jade Philipoom2018-04-03
* progress on from_columns proofsGravatar Jade Philipoom2018-04-03
* clean up proofs a bitGravatar Jade Philipoom2018-04-03
* prove sum_rows_div_mod and fix up Rows.from_columns a bitGravatar Jade Philipoom2018-04-03
* rowwise flatten (more fleshed-out) and proof outlineGravatar Jade Philipoom2018-04-03
* preliminary version of rowwise flattenGravatar Jade Philipoom2018-04-03
* some work on rowwise flattenGravatar Jade Philipoom2018-04-03
* Add two examples of using the pipeline in a one-linerGravatar Jason Gross2018-04-01
* Fix the pipeline to not insert extra castsGravatar Jason Gross2018-03-31
* Update printout after change to pipelineGravatar Jason Gross2018-03-31
* Do some pipeline consolidation and reorganizationGravatar Jason Gross2018-03-29
* Allow passing in optional bounds to the pipelineGravatar Jason Gross2018-03-28
* Inline weight into *mod, remove rweightGravatar Jason Gross2018-03-28
* Move mod_ops out of PositionalGravatar Jason Gross2018-03-28
* Move cps out of cache part of the pipelineGravatar Jason Gross2018-03-27
* Add Zdiv_0_l to zsimplify dbsGravatar Jason Gross2018-03-27
* Add a test for hd and tlGravatar Jason Gross2018-03-27
* Add support for handling match on listGravatar Jason Gross2018-03-27
* Add list_case, a definition for match on listGravatar Jason Gross2018-03-27
* Response to code review commentGravatar Jason Gross2018-03-23
* Be more explicit about reductionGravatar Jason Gross2018-03-23
* s/nobrainer1/subst01/Gravatar Jason Gross2018-03-23
* Remove spurious indentationGravatar Jason Gross2018-03-23
* Added input var type for clarityGravatar Jason Gross2018-03-23
* Make the ERROR definition opaque to vm_computeGravatar Jason Gross2018-03-23
* Add GeneralizeVar explanatory commentGravatar Jason Gross2018-03-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 04:37:51 +0000