blob: 4093a79bffcaeaa32ca71f3cc8cd97cb1bb153a2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
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).
|
