From 47d1b325f227b75a912ec560624f524ce9d04edf Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 3 Mar 2022 19:27:26 +0000 Subject: Add cast operation --- src/BitEQ.v | 11 +++++++++++ 1 file changed, 11 insertions(+) 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). -- cgit