source: extracted/bitVectorTrieSet.mli @ 2746

Last change on this file since 2746 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 871 bytes
Line 
1open Preamble
2
3open Extranat
4
5open Vector
6
7open Div_and_mod
8
9open Jmeq
10
11open Russell
12
13open List
14
15open Util
16
17open FoldStuff
18
19open Bool
20
21open Relations
22
23open Nat
24
25open BitVector
26
27open Hints_declaration
28
29open Core_notation
30
31open Pts
32
33open Logic
34
35open Types
36
37open BitVectorTrie
38
39type bitVectorTrieSet = Types.unit0 BitVectorTrie.bitVectorTrie
40
41val set_member :
42  Nat.nat -> Bool.bool Vector.vector -> bitVectorTrieSet -> Bool.bool
43
44val set_union :
45  Nat.nat -> bitVectorTrieSet -> bitVectorTrieSet -> bitVectorTrieSet
46
47val set_eq : Nat.nat -> bitVectorTrieSet -> bitVectorTrieSet -> Bool.bool
48
49val set_insert :
50  Nat.nat -> BitVector.bitVector -> bitVectorTrieSet -> Types.unit0
51  BitVectorTrie.bitVectorTrie
52
53val set_empty : Nat.nat -> Types.unit0 BitVectorTrie.bitVectorTrie
54
55val set_singleton :
56  Nat.nat -> BitVector.bitVector -> Types.unit0 BitVectorTrie.bitVectorTrie
57
Note: See TracBrowser for help on using the repository browser.