extracted/bitVectorZ.mli

   1 open Preamble
   2
   3 open Types
   4
   5 open Bool
   6
   7 open Relations
   8
   9 open Nat
  10
  11 open Hints_declaration
  12
  13 open Core_notation
  14
  15 open Pts
  16
  17 open Logic
  18
  19 open Positive
  20
  21 open Z
  22
  23 open Setoids
  24
  25 open Monad
  26
  27 open Option
  28
  29 open Extranat
  30
  31 open Vector
  32
  33 open Div_and_mod
  34
  35 open Jmeq
  36
  37 open Russell
  38
  39 open List
  40
  41 open Util
  42
  43 open FoldStuff
  44
  45 open BitVector
  46
  47 open Exp
  48
  49 open Arithmetic
  50
  51 open Division
  52
  53 val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z
  54
  55 val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z
  56
  57 val bits_of_pos : Positive.pos -> Bool.bool List.list
  58
  59 val zeroext_reversed :
  60   Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
  61
  62 val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector
  63
  64 val pos_length : Positive.pos -> Nat.nat
  65