diff options
Diffstat (limited to 'src/Util/BoundedWord.v')
-rw-r--r-- | src/Util/BoundedWord.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/BoundedWord.v b/src/Util/BoundedWord.v index cfd27a231..e5c3720fe 100644 --- a/src/Util/BoundedWord.v +++ b/src/Util/BoundedWord.v @@ -5,8 +5,8 @@ Require Import Crypto.Util.FixedWordSizes. Definition BoundedWord n (bitwidth : nat) (bounds : tuple zrange n) : Type := - { x : tuple (wordT bitwidth) n - | is_bounded_by (Some (Z.of_nat bitwidth)) bounds + { x : tuple (wordT (Nat.log2 bitwidth)) n + | is_bounded_by None bounds (map wordToZ x)}. Definition BoundedWordToZ n w b (BW :BoundedWord n w b) |