diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-31 20:21:28 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-10-31 20:21:28 -0400 |
commit | efb855b7ca6c9a917fd0c5993f29d3856185ce5f (patch) | |
tree | e95d358b3cd45ea3d906c2b5fbe08da42c478c85 /Bedrock | |
parent | ca2f096f268a4cac94c2c1999c4ad1e7b6e2f002 (diff) |
Add Bedrock.Word.ZToWord
Diffstat (limited to 'Bedrock')
-rw-r--r-- | Bedrock/Word.v | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/Bedrock/Word.v b/Bedrock/Word.v index 2726a03c3..016903a7f 100644 --- a/Bedrock/Word.v +++ b/Bedrock/Word.v @@ -1001,7 +1001,7 @@ Ltac word_contra1 := match goal with Open Scope word_scope. (** * Signed Logic **) -Fixpoint wordToZ sz (w : word sz) : Z := +Definition wordToZ sz (w : word sz) : Z := if wmsb w true then (** Negative **) match wordToN (wneg w) with @@ -1014,6 +1014,13 @@ Fixpoint wordToZ sz (w : word sz) : Z := | N0 => 0%Z | Npos x => Zpos x end. +Definition ZToWord sz (v : Z) : word sz := + if (v <? 0)%Z then + (** Negative **) + wneg (NToWord (Z.to_N (-v))) + else + (** Positive **) + wordToN (Z.to_N v). (** * Comparison Predicates and Deciders **) Definition wlt sz (l r : word sz) : Prop := |