diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-03 14:09:42 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-03 14:09:42 -0500 |
| commit | cd496376a5f237340d7daff1bae8f23004d5358a (patch) | |
| tree | 779b1af4fb9dd76577358bf4238c1aa5e4ac7f8d | |
| parent | a66ba3e5202adcc436c3a1fcf6433261e7bdd158 (diff) | |
Revert "Add Bedrock.Word.{wordToZ,ZToWord}"
This reverts commit a66ba3e5202adcc436c3a1fcf6433261e7bdd158.
| -rw-r--r-- | Bedrock/Word.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/Bedrock/Word.v b/Bedrock/Word.v index 1744f80ef..2c518807d 100644 --- a/Bedrock/Word.v +++ b/Bedrock/Word.v @@ -1,6 +1,6 @@ (** Fixed precision machine words *) -Require Import Coq.ZArith.ZArith Coq.Arith.Arith Coq.Arith.Div2 Coq.NArith.NArith Coq.Bool.Bool Coq.omega.Omega. +Require Import Coq.Arith.Arith Coq.Arith.Div2 Coq.NArith.NArith Coq.Bool.Bool Coq.omega.Omega. Require Import Bedrock.Nomega. Set Implicit Arguments. @@ -84,9 +84,6 @@ Definition NToWord (sz : nat) (n : N) : word sz := | Npos p => posToWord sz p end. -Definition ZToWord sz (n : Z) : word sz := NToWord sz (Z.to_N n). -Definition wordToZ sz (w : word sz) : Z := Z.of_N (wordToN w). - Fixpoint Npow2 (n : nat) : N := match n with | O => 1 |