Add Bedrock.Word.{wordToZ,ZToWord}

1 files changed, 4 insertions, 1 deletions

diff --git a/Bedrock/Word.v b/Bedrock/Word.v
index 2c518807d..1744f80ef 100644
--- a/Bedrock/Word.v
+++ b/Bedrock/Word.v
@@ -1,6 +1,6 @@
 (** Fixed precision machine words *)
 
-Require Import Coq.Arith.Arith Coq.Arith.Div2 Coq.NArith.NArith Coq.Bool.Bool Coq.omega.Omega.
+Require Import Coq.ZArith.ZArith Coq.Arith.Arith Coq.Arith.Div2 Coq.NArith.NArith Coq.Bool.Bool Coq.omega.Omega.
 Require Import Bedrock.Nomega.
 
 Set Implicit Arguments.
@@ -84,6 +84,9 @@ 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