aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Fix a name clashGravatar Jason Gross2017-03-14
* Add firstn_skipnGravatar Jason Gross2017-03-14
* Add split_prodGravatar Jason Gross2017-03-14
* Add skipn_skipnGravatar Jason Gross2017-03-14
* Move find_if_eq to Decidable.v, use Decidable in NamedGravatar Jason Gross2017-03-14
* Add faster versions of destruct_head_*Gravatar Jason Gross2017-03-14
* address some code review commentsGravatar Andres Erbsen2017-03-02
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* Add η principles for sigma typesGravatar Jason Gross2017-03-01
* Add dlet_nd notationGravatar Jason Gross2017-03-01
* Add strip_eta_tuple lemmasGravatar Jason Gross2017-02-28
* Better tuple_eta argumentsGravatar Jason Gross2017-02-28
* Add eta_tuple functionsGravatar Jason Gross2017-02-28
* Added operation (including creating )Gravatar jadep2017-02-27
* added Positional wrappers for Associational operations, added correctness pro...Gravatar jadep2017-02-27
* Modified lemma and created tactic to handle it; added reduce step to multipl...Gravatar jadep2017-02-26
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 17:17:50 +0000