diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-30 18:41:49 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-30 18:42:10 -0400 |
| commit | 598ae72e8653a20cfa3e1ded0d6e1aedf6323f18 (patch) | |
| tree | cee8b5df46abb743f9a38de2ff59b9fcdea7e12d | |
| parent | aefe2925f8f1920276fb47091379472785ef3103 (diff) | |
Add wordToZ{_gen,}_range
| -rw-r--r-- | src/Util/FixedWordSizesEquality.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v index 8c5b1ead0..e1a8f1f79 100644 --- a/src/Util/FixedWordSizesEquality.v +++ b/src/Util/FixedWordSizesEquality.v @@ -262,6 +262,13 @@ Ltac fixed_size_op_to_word := repeat autounfold with fixed_size_constants in *; syntactic_fixed_size_op_to_word. +Lemma wordToZ_gen_range {sz} w : (0 <= @wordToZ_gen sz w < 2^Z.of_nat sz)%Z. +Proof. apply WordNZ_range; reflexivity. Qed. + +Lemma wordToZ_range {logsz} w : (0 <= @wordToZ logsz w < 2^Z.of_nat (2^logsz))%Z. +Proof. + generalize (@wordToZ_gen_range (2^logsz)); wordToZ_word_case_dep_t. +Qed. Section log_Updates. Local Notation bound n lower value upper := ( |