aboutsummaryrefslogtreecommitdiff
path: root/src/Util/FixedWordSizes.v
Commit message (Collapse)AuthorAge
* Remove BoundedWordGravatar Benjamin Barenblat2019-04-26
| | | | | | Remove Util/BoundedWord.v and its reverse dependencies Util/FixedWordSizes.v and Util/FixedWordSizesEquality.v. This code is no longer in use.
* minor updates needed to make it compile with bbvGravatar Samuel Gruetter2018-02-05
| | | | removing lemma wordToNat_wzero is ok because it's already in bbv
* add ZToSignedWord, signedWordToZGravatar Jason Gross2017-10-31
|
* Don't autounfold wordToZ nor ZToWordGravatar Jason Gross2017-02-03
| | | | The tactic fixed_size_op_to_word relies on them being folded.
* Add fixed_size_op_to_word tacticGravatar Jason Gross2017-02-03
|
* Better word operationsGravatar Jason Gross2017-01-03
|
* Add ZToWord,wordToZGravatar Jason Gross2017-01-03
|
* Add fixed word size definitionsGravatar Jason Gross2017-01-03