source: driver/extracted/bitVectorTrie.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: 3.7 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Setoids
14
15open Monad
16
17open Option
18
19open Extranat
20
21open Vector
22
23open Div_and_mod
24
25open Jmeq
26
27open Russell
28
29open List
30
31open Util
32
33open FoldStuff
34
35open Bool
36
37open Relations
38
39open Nat
40
41open BitVector
42
43type 'a bitVectorTrie =
44| Leaf of 'a
45| Node of Nat.nat * 'a bitVectorTrie * 'a bitVectorTrie
46| Stub of Nat.nat
47
48val bitVectorTrie_rect_Type4 :
49  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
50  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
51
52val bitVectorTrie_rect_Type3 :
53  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
54  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
55
56val bitVectorTrie_rect_Type2 :
57  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
58  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
59
60val bitVectorTrie_rect_Type1 :
61  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
62  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
63
64val bitVectorTrie_rect_Type0 :
65  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
66  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
67
68val bitVectorTrie_inv_rect_Type4 :
69  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
70  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
71  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
72
73val bitVectorTrie_inv_rect_Type3 :
74  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
75  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
76  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
77
78val bitVectorTrie_inv_rect_Type2 :
79  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
80  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
81  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
82
83val bitVectorTrie_inv_rect_Type1 :
84  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
85  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
86  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
87
88val bitVectorTrie_inv_rect_Type0 :
89  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
90  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
91  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
92
93val bitVectorTrie_discr :
94  Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __
95
96val bitVectorTrie_jmdiscr :
97  Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __
98
99val fold :
100  Nat.nat -> (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a1 bitVectorTrie
101  -> 'a2 -> 'a2
102
103val bvtfold_aux :
104  (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> Nat.nat -> 'a1
105  bitVectorTrie -> BitVector.bitVector -> 'a2
106
107val lookup_opt :
108  Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 Types.option
109
110val member : Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> Bool.bool
111
112val lookup :
113  Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 -> 'a1
114
115val prepare_trie_for_insertion :
116  Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie
117
118val insert :
119  Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
120  bitVectorTrie
121
122val update :
123  Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
124  bitVectorTrie Types.option
125
126val merge :
127  Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie
128
129open Deqsets
130
131type strong_decidable = (__, __) Types.sum
132
133val strong_decidable_in_codomain :
134  Deqsets.deqSet -> Nat.nat -> __ bitVectorTrie -> __ -> strong_decidable
135
Note: See TracBrowser for help on using the repository browser.