diff options
| author |  Benjamin Barenblat <bbaren@google.com> | 2019-04-26 16:33:54 -0400 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@google.com> | 2019-04-26 16:33:54 -0400 |
| commit | d20b2cbc862fb35b5e059cbfafaaa9360fb6afce (patch) | |
| tree | 03fbcdecba17f92b4354df6ef30de9c1821d154d /src/Util/BoundedWord.v | |
| parent | e93ec9a4112d2a6f78deb8fca10c5bd5c4b3c1cb (diff) | |
Remove BoundedWord
Remove Util/BoundedWord.v and its reverse dependencies
Util/FixedWordSizes.v and Util/FixedWordSizesEquality.v. This code is no
longer in use.
Diffstat (limited to 'src/Util/BoundedWord.v')
| -rw-r--r-- | src/Util/BoundedWord.v | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/src/Util/BoundedWord.v b/src/Util/BoundedWord.v deleted file mode 100644 index e5c3720fe..000000000 --- a/src/Util/BoundedWord.v +++ /dev/null @@ -1,13 +0,0 @@ -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 (Nat.log2 bitwidth)) n - | is_bounded_by None bounds - (map wordToZ x)}. - -Definition BoundedWordToZ n w b (BW :BoundedWord n w b) - : tuple Z n := map wordToZ (proj1_sig BW). |