diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-03 19:27:26 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-03 19:27:26 +0000 |
| commit | 47d1b325f227b75a912ec560624f524ce9d04edf (patch) | |
| tree | c2a525cceba3061db6762697d9636e28056e974b | |
| parent | c41ecea1938a16d10cef797ce2e0cdbb38f15a1b (diff) | |
| download | biteq-47d1b325f227b75a912ec560624f524ce9d04edf.tar.gz biteq-47d1b325f227b75a912ec560624f524ce9d04edf.zip | |
Add cast operation
| -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). |