diff options
| -rw-r--r-- | src/BitEQ.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/BitEQ.v b/src/BitEQ.v index f648f40..4093a79 100644 --- a/src/BitEQ.v +++ b/src/BitEQ.v @@ -1 +1,12 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Coq.Bool.Bool. + Require Import bbv.Word. +Import Notations. + +#[local] Open Scope nat_scope. +#[local] Open Scope word_scope. + +Definition wucast {sz: nat} (sz': nat) (w: word sz) : word sz' := + ZToWord _ (uwordToZ w). |