diff options
Diffstat (limited to 'src/Specific/IntegrationTest.v')
| -rw-r--r-- | src/Specific/IntegrationTest.v | 13 |
1 files changed, 1 insertions, 12 deletions
diff --git a/src/Specific/IntegrationTest.v b/src/Specific/IntegrationTest.v index 39f34a311..49fb55969 100644 --- a/src/Specific/IntegrationTest.v +++ b/src/Specific/IntegrationTest.v @@ -7,20 +7,9 @@ Require Import Crypto.NewBaseSystem. Require Import Crypto.Util.FixedWordSizes. Require Import Crypto.Specific.NewBaseSystemTest. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Notations Crypto.Util.ZRange. +Require Import Crypto.Util.Tuple Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. Import ListNotations. -Section Pre. - 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). -End Pre. - Section BoundedField25p5. Local Coercion Z.of_nat : nat >-> Z. |