From a66ba3e5202adcc436c3a1fcf6433261e7bdd158 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 3 Jan 2017 14:08:51 -0500 Subject: Add Bedrock.Word.{wordToZ,ZToWord} --- Bedrock/Word.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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 -- cgit v1.2.3