aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
...
* speed up NewBaseystem synthesisGravatar Andres Erbsen2017-02-23
* Add log and non-log versions of FixedWordSizes lemGravatar Jason Gross2017-02-23
* Add invert_Some; add nat_N_Z to push_Zof_NGravatar Jason Gross2017-02-23
* move lemmas from Ed25519 to WordUtilGravatar jadep2017-02-22
* move some lemmas from Ed25519 to ZUtilGravatar jadep2017-02-22
* moved more stuff to NUtilGravatar jadep2017-02-22
* Moved N lemmas from Ed25519 and IterAssocOp into new NUtil fileGravatar jadep2017-02-22
* Merge new base system (#112)Gravatar jadephilipoom2017-02-22
* Factor things into BoundByCast.vGravatar Jason Gross2017-02-08
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 03:20:47 +0000