extracted/bitVectorTrieSet.mli

   1 open Preamble
   2
   3 open Deqsets
   4
   5 open Setoids
   6
   7 open Monad
   8
   9 open Option
  10
  11 open Extranat
  12
  13 open Vector
  14
  15 open Div_and_mod
  16
  17 open Jmeq
  18
  19 open Russell
  20
  21 open List
  22
  23 open Util
  24
  25 open FoldStuff
  26
  27 open Bool
  28
  29 open Relations
  30
  31 open Nat
  32
  33 open BitVector
  34
  35 open Hints_declaration
  36
  37 open Core_notation
  38
  39 open Pts
  40
  41 open Logic
  42
  43 open Types
  44
  45 open BitVectorTrie
  46
  47 type bitVectorTrieSet = Types.unit0 BitVectorTrie.bitVectorTrie
  48
  49 val set_member :
  50   Nat.nat -> Bool.bool Vector.vector -> bitVectorTrieSet -> Bool.bool
  51
  52 val set_union :
  53   Nat.nat -> bitVectorTrieSet -> bitVectorTrieSet -> bitVectorTrieSet
  54
  55 val set_eq : Nat.nat -> bitVectorTrieSet -> bitVectorTrieSet -> Bool.bool
  56
  57 val set_insert :
  58   Nat.nat -> BitVector.bitVector -> bitVectorTrieSet -> Types.unit0
  59   BitVectorTrie.bitVectorTrie
  60
  61 val set_empty : Nat.nat -> Types.unit0 BitVectorTrie.bitVectorTrie
  62
  63 val set_singleton :
  64   Nat.nat -> BitVector.bitVector -> Types.unit0 BitVectorTrie.bitVectorTrie
  65