aboutsummaryrefslogtreecommitdiff
path: root/src/Util/FixedWordSizesEquality.v
Commit message (Expand)AuthorAge
* Add wordToZ{_gen,}_rangeGravatar Jason Gross2017-03-30
* Add log and non-log versions of FixedWordSizes lemGravatar Jason Gross2017-02-23
* 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
* 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
* Add fixed_size_op_to_word tacticGravatar Jason Gross2017-02-03
* Add wordToZ_ZToWord_wordToZGravatar Jason Gross2017-02-01
* Add ZToWord_wordToZ_ZToWordGravatar Jason Gross2017-02-01
* Add wordToZ_ZToWord, ZToWord_wordToZGravatar Jason Gross2017-02-01
* Add transparent equality proofs for fixed wordTGravatar Jason Gross2017-01-21