extracted/bitVector.mli

   1 open Preamble
   2
   3 open Bool
   4
   5 open Hints_declaration
   6
   7 open Core_notation
   8
   9 open Pts
  10
  11 open Logic
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open Div_and_mod
  18
  19 open Jmeq
  20
  21 open Russell
  22
  23 open Types
  24
  25 open List
  26
  27 open Util
  28
  29 open FoldStuff
  30
  31 open Setoids
  32
  33 open Monad
  34
  35 open Option
  36
  37 open Extranat
  38
  39 open Vector
  40
  41 type bitVector = Bool.bool Vector.vector
  42
  43 type bit = Bool.bool
  44
  45 type nibble = bitVector
  46
  47 type byte7 = bitVector
  48
  49 type byte = bitVector
  50
  51 type word = bitVector
  52
  53 type word11 = bitVector
  54
  55 val zero : Nat.nat -> bitVector
  56
  57 val maximum : Nat.nat -> bitVector
  58
  59 val pad : Nat.nat -> Nat.nat -> bitVector -> Bool.bool Vector.vector
  60
  61 val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector
  62
  63 val inclusive_disjunction_bv :
  64   Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector
  65
  66 val exclusive_disjunction_bv :
  67   Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector
  68
  69 val negation_bv : Nat.nat -> bitVector -> Bool.bool Vector.vector
  70
  71 val eq_b : Bool.bool -> Bool.bool -> Bool.bool
  72
  73 val eq_bv : Nat.nat -> bitVector -> bitVector -> Bool.bool
  74
  75 val eq_bv_elim :
  76   Nat.nat -> bitVector -> bitVector -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  77