11 open Hints_declaration
53 val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z
55 val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z
57 val bits_of_pos : Positive.pos -> Bool.bool List.list
59 val zeroext_reversed :
60 Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
62 val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector
64 val pos_length : Positive.pos -> Nat.nat