aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Add match commutation lemmasGravatar Jason Gross2017-01-23
* Minor additionsGravatar Jason Gross2017-01-23
* Add transparent equality proofs for fixed wordTGravatar Jason Gross2017-01-21
* Revert "Fix a missing qualification"Gravatar Jason Gross2017-01-21
* Fix a missing qualificationGravatar Jason Gross2017-01-21
* Move weqb_hetero to Bedrock.WordGravatar Jason Gross2017-01-21
* Add weqb_heteroGravatar Jason Gross2017-01-21
* Add split_andb tacticGravatar Jason Gross2017-01-21
* Update notations from zetabaseGravatar Jason Gross2017-01-19
* Add ZUtil lemma from zetabaseGravatar Jason Gross2017-01-19
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Add nat_beq_to_eqGravatar Jason Gross2017-01-19
* Fix infinite loop in destruct_rewrite_sumboolGravatar Jason Gross2017-01-17
* More fine-grained util tactic filesGravatar Jason Gross2017-01-17
* Use match in curry2; this gives better reificationGravatar Jason Gross2017-01-15
* Add curry.vGravatar Jason Gross2017-01-15
* More universe fixesGravatar Jason Gross2017-01-15
* Fix an issue with universesGravatar Jason Gross2017-01-15
* Add >>> reserved notationGravatar Jason Gross2017-01-09
* Add Zmod_to_equiv_moduloGravatar Jason Gross2017-01-09
* Revert "Add apply10"Gravatar Jason Gross2017-01-07
* Add apply10Gravatar Jason Gross2017-01-07
* Better word operationsGravatar Jason Gross2017-01-03
* Add ZToWord,wordToZGravatar Jason Gross2017-01-03
* Add fixed word size definitionsGravatar Jason Gross2017-01-03
* Work around bug in 8.4 applyGravatar Jason Gross2016-12-14
* More powerful inversion_optionGravatar Jason Gross2016-12-03
* Add tuple lemmasGravatar Jason Gross2016-11-22
* Add impl_under_towerGravatar Jason Gross2016-11-22
* Add hlistPGravatar Jason Gross2016-11-22
* Add rhlistGravatar Jason Gross2016-11-22
* Add tower_ndGravatar Jason Gross2016-11-22
* Add fieldwise_mapGravatar Jason Gross2016-11-17
* Add HList.mapt_ProperGravatar Jason Gross2016-11-17
* Update AddCoordinatesGravatar Jason Gross2016-11-17
* Move util definitions to util folderGravatar Jason Gross2016-11-17
* Add fieldwise_eq_edwards_extended_add_coordinates_carry_nocarryGravatar Jason Gross2016-11-17
* use @implicits in rewrite (8.4)Gravatar Andres Erbsen2016-11-11
* Lemmas about winit, wlastGravatar Rob Sloan2016-11-11
* prove last HList admitGravatar Andres Erbsen2016-11-11
* prove admits in Util.TupleGravatar Andres Erbsen2016-11-11
* Fix for Coq 8.4Gravatar Jason Gross2016-11-11
* Most of the admits in Ed25519.vGravatar Rob Sloan2016-11-11
* Add Tuple and HList lemmasGravatar Jason Gross2016-11-10
* Fix for 8.4Gravatar Jason Gross2016-11-10
* Hint Rewrite is section-local; move to top-levelGravatar Jason Gross2016-11-10
* Remove WordizeUtil dependency from WordUtilGravatar Rob Sloan2016-11-09
* Rebase + remove WordizeUtil dependency from Z/InterpretationsGravatar Rob Sloan2016-11-09
|\
| * Rewrite cast_word so that it's extracted betterGravatar Jason Gross2016-11-09
| * Fix bug in 8.4Gravatar Jason Gross2016-11-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 08:15:02 +0000