source: driver/extracted/bitVectorTrieSet.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 924 bytes
Line 
1open Preamble
2
3open Deqsets
4
5open Setoids
6
7open Monad
8
9open Option
10
11open Extranat
12
13open Vector
14
15open Div_and_mod
16
17open Jmeq
18
19open Russell
20
21open List
22
23open Util
24
25open FoldStuff
26
27open Bool
28
29open Relations
30
31open Nat
32
33open BitVector
34
35open Hints_declaration
36
37open Core_notation
38
39open Pts
40
41open Logic
42
43open Types
44
45open BitVectorTrie
46
47type bitVectorTrieSet = Types.unit0 BitVectorTrie.bitVectorTrie
48
49val set_member :
50  Nat.nat -> Bool.bool Vector.vector -> bitVectorTrieSet -> Bool.bool
51
52val set_union :
53  Nat.nat -> bitVectorTrieSet -> bitVectorTrieSet -> bitVectorTrieSet
54
55val set_eq : Nat.nat -> bitVectorTrieSet -> bitVectorTrieSet -> Bool.bool
56
57val set_insert :
58  Nat.nat -> BitVector.bitVector -> bitVectorTrieSet -> Types.unit0
59  BitVectorTrie.bitVectorTrie
60
61val set_empty : Nat.nat -> Types.unit0 BitVectorTrie.bitVectorTrie
62
63val set_singleton :
64  Nat.nat -> BitVector.bitVector -> Types.unit0 BitVectorTrie.bitVectorTrie
65
Note: See TracBrowser for help on using the repository browser.