source: driver/extracted/identifiers.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: 8.8 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open Nat
18
19open Positive
20
21open Setoids
22
23open Monad
24
25open Option
26
27open Div_and_mod
28
29open Jmeq
30
31open Russell
32
33open Util
34
35open List
36
37open Lists
38
39open Extralib
40
41open ErrorMessages
42
43open PreIdentifiers
44
45open Errors
46
47type universe =
48  Positive.pos
49  (* singleton inductive, whose constructor was mk_universe *)
50
51val universe_rect_Type4 :
52  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
53
54val universe_rect_Type5 :
55  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
56
57val universe_rect_Type3 :
58  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
59
60val universe_rect_Type2 :
61  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
62
63val universe_rect_Type1 :
64  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
65
66val universe_rect_Type0 :
67  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
68
69val next_identifier :
70  PreIdentifiers.identifierTag -> universe -> Positive.pos
71
72val universe_inv_rect_Type4 :
73  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
74  'a1
75
76val universe_inv_rect_Type3 :
77  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
78  'a1
79
80val universe_inv_rect_Type2 :
81  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
82  'a1
83
84val universe_inv_rect_Type1 :
85  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
86  'a1
87
88val universe_inv_rect_Type0 :
89  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
90  'a1
91
92val universe_discr :
93  PreIdentifiers.identifierTag -> universe -> universe -> __
94
95val universe_jmdiscr :
96  PreIdentifiers.identifierTag -> universe -> universe -> __
97
98val new_universe : PreIdentifiers.identifierTag -> universe
99
100val fresh :
101  PreIdentifiers.identifierTag -> universe -> (PreIdentifiers.identifier,
102  universe) Types.prod
103
104val eq_identifier :
105  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
106  PreIdentifiers.identifier -> Bool.bool
107
108val eq_identifier_elim :
109  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
110  PreIdentifiers.identifier -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
111
112open Deqsets
113
114val deq_identifier : PreIdentifiers.identifierTag -> Deqsets.deqSet
115
116val word_of_identifier :
117  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> Positive.pos
118
119val identifier_eq :
120  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
121  PreIdentifiers.identifier -> (__, __) Types.sum
122
123val identifier_of_nat :
124  PreIdentifiers.identifierTag -> Nat.nat -> PreIdentifiers.identifier
125
126val check_member_env :
127  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
128  (PreIdentifiers.identifier, 'a1) Types.prod List.list -> __ Errors.res
129
130val check_distinct_env :
131  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier, 'a1) Types.prod
132  List.list -> __ Errors.res
133
134open PositiveMap
135
136type 'a identifier_map =
137  'a PositiveMap.positive_map
138  (* singleton inductive, whose constructor was an_id_map *)
139
140val identifier_map_rect_Type4 :
141  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
142  'a1 identifier_map -> 'a2
143
144val identifier_map_rect_Type5 :
145  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
146  'a1 identifier_map -> 'a2
147
148val identifier_map_rect_Type3 :
149  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
150  'a1 identifier_map -> 'a2
151
152val identifier_map_rect_Type2 :
153  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
154  'a1 identifier_map -> 'a2
155
156val identifier_map_rect_Type1 :
157  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
158  'a1 identifier_map -> 'a2
159
160val identifier_map_rect_Type0 :
161  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
162  'a1 identifier_map -> 'a2
163
164val identifier_map_inv_rect_Type4 :
165  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
166  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
167
168val identifier_map_inv_rect_Type3 :
169  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
170  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
171
172val identifier_map_inv_rect_Type2 :
173  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
174  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
175
176val identifier_map_inv_rect_Type1 :
177  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
178  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
179
180val identifier_map_inv_rect_Type0 :
181  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
182  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
183
184val identifier_map_discr :
185  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
186  __
187
188val identifier_map_jmdiscr :
189  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
190  __
191
192val empty_map : PreIdentifiers.identifierTag -> 'a1 identifier_map
193
194val lookup :
195  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
196  PreIdentifiers.identifier -> 'a1 Types.option
197
198val lookup_def :
199  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
200  PreIdentifiers.identifier -> 'a1 -> 'a1
201
202val member :
203  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
204  PreIdentifiers.identifier -> Bool.bool
205
206val lookup_safe :
207  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
208  PreIdentifiers.identifier -> 'a1
209
210val add :
211  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
212  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map
213
214val elements :
215  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
216  (PreIdentifiers.identifier, 'a1) Types.prod List.list
217
218val idmap_all :
219  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
220  (PreIdentifiers.identifier -> 'a1 -> __ -> Bool.bool) -> Bool.bool
221
222val update :
223  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
224  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map Errors.res
225
226val remove :
227  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
228  PreIdentifiers.identifier -> 'a1 identifier_map
229
230val foldi :
231  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> 'a1 -> 'a2 ->
232  'a2) -> 'a1 identifier_map -> 'a2 -> 'a2
233
234val fold_inf :
235  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
236  (PreIdentifiers.identifier -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2
237
238val find :
239  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
240  (PreIdentifiers.identifier -> 'a1 -> Bool.bool) ->
241  (PreIdentifiers.identifier, 'a1) Types.prod Types.option
242
243val lookup_present :
244  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
245  PreIdentifiers.identifier -> 'a1
246
247val update_present :
248  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
249  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map
250
251type identifier_set = Types.unit0 identifier_map
252
253val empty_set : PreIdentifiers.identifierTag -> identifier_set
254
255val add_set :
256  PreIdentifiers.identifierTag -> identifier_set -> PreIdentifiers.identifier
257  -> identifier_set
258
259val singleton_set :
260  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier_set
261
262val union_set :
263  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
264  identifier_set
265
266val minus_set :
267  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
268  'a1 identifier_map
269
270val identifierSet : PreIdentifiers.identifierTag -> Setoids.setoid
271
272val id_map_size :
273  PreIdentifiers.identifierTag -> 'a1 identifier_map -> Nat.nat
274
275open Proper
276
277val set_from_list :
278  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
279  Types.unit0 identifier_map
280
281val dpi1__o__id_set_from_list__o__inject :
282  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list, 'a1)
283  Types.dPair -> Types.unit0 identifier_map Types.sig0
284
285val eject__o__id_set_from_list__o__inject :
286  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
287  Types.sig0 -> Types.unit0 identifier_map Types.sig0
288
289val id_set_from_list__o__inject :
290  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
291  Types.unit0 identifier_map Types.sig0
292
293val dpi1__o__id_set_from_list :
294  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list, 'a1)
295  Types.dPair -> Types.unit0 identifier_map
296
297val eject__o__id_set_from_list :
298  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
299  Types.sig0 -> Types.unit0 identifier_map
300
301val choose :
302  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
303  ((PreIdentifiers.identifier, 'a1) Types.prod, 'a1 identifier_map)
304  Types.prod Types.option
305
306val try_remove :
307  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
308  PreIdentifiers.identifier -> ('a1, 'a1 identifier_map) Types.prod
309  Types.option
310
311val id_set_of_map :
312  PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set
313
314val set_of_list :
315  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
316  identifier_set
317
318val domain_of_map :
319  PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set
320
Note: See TracBrowser for help on using the repository browser.