aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Add ZUtil lemmasGravatar Jason Gross2017-02-06
* Move things from WordUtil to ZUtil, add word lemmaGravatar Jason Gross2017-02-06
* Split off non-unfolding version of fixed_size_op_to_wordGravatar Jason Gross2017-02-03
* Add valid_update lemmas about FixedWordSizesGravatar Jason Gross2017-02-03
* Don't unfold wordToZ_gen in fixed_Size_op_to_wordGravatar Jason Gross2017-02-03
* More zutilGravatar Jason Gross2017-02-03
* Add lemmas about bounds of Z.lor, and add Z.max_log2_upGravatar Jason Gross2017-02-03
* Fix a missing argumentGravatar Jason Gross2017-02-03
* Fix a typoGravatar Jason Gross2017-02-03
* Handle more kinds of ops in fixed_size_op_to_wordGravatar Jason Gross2017-02-03
* Don't autounfold wordToZ nor ZToWordGravatar Jason Gross2017-02-03
* Add fixed_size_op_to_word tacticGravatar Jason Gross2017-02-03
* Add lemmas for Z ops ProperGravatar Jason Gross2017-02-03
* Add log2_up_le_fullGravatar Jason Gross2017-02-03
* Add Z.log2_up_nonneg to zarithGravatar Jason Gross2017-02-03
* Add wordToZ_ZToWord_wordToZGravatar Jason Gross2017-02-01
* Add ZToWord_wordToZ_ZToWordGravatar Jason Gross2017-02-01
* Add NToWord_wordToN_NToWordGravatar Jason Gross2017-02-01
* Add wordToZ_ZToWord, ZToWord_wordToZGravatar Jason Gross2017-02-01
* Add inversion_exprGravatar Jason Gross2017-02-01
* Split off unique {pose,assert}Gravatar Jason Gross2017-01-31
* Don't change sumbool eq hypothesis unless both sides are constructorsGravatar Jason Gross2017-01-30
* Fix typosGravatar Jason Gross2017-01-30
* Add Util.SumboolGravatar Jason Gross2017-01-30
* Split off some bits of Reflection.SyntaxGravatar Jason Gross2017-01-26
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 16:01:56 +0000