open Preamble

open Types

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

open Z

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open BitVector

open Exp

open Arithmetic

open Division

val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z

val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z

val bits_of_pos : Positive.pos -> Bool.bool List.list

val zeroext_reversed :
  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector

val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector

val pos_length : Positive.pos -> Nat.nat