blob: cfd27a2317d84fbf0fdc0281cd88ad0634c5a97d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.ZRange.
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
(map wordToZ x)}.
Definition BoundedWordToZ n w b (BW :BoundedWord n w b)
: tuple Z n := map wordToZ (proj1_sig BW).
|
