source: extracted/identifiers.mli @ 2960

Last change on this file since 2960 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
RevLine 
[2601]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
[2649]35open List
36
[2601]37open Lists
38
39open Extralib
40
[2649]41open ErrorMessages
42
[2601]43open PreIdentifiers
44
45open Errors
46
47type universe =
48  Positive.pos
49  (* singleton inductive, whose constructor was mk_universe *)
50
51val universe_rect_Type4 :
[2649]52  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
[2601]53
54val universe_rect_Type5 :
[2649]55  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
[2601]56
57val universe_rect_Type3 :
[2649]58  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
[2601]59
60val universe_rect_Type2 :
[2649]61  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
[2601]62
63val universe_rect_Type1 :
[2649]64  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
[2601]65
66val universe_rect_Type0 :
[2649]67  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
[2601]68
[2649]69val next_identifier :
70  PreIdentifiers.identifierTag -> universe -> Positive.pos
[2601]71
72val universe_inv_rect_Type4 :
[2649]73  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
74  'a1
[2601]75
76val universe_inv_rect_Type3 :
[2649]77  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
78  'a1
[2601]79
80val universe_inv_rect_Type2 :
[2649]81  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
82  'a1
[2601]83
84val universe_inv_rect_Type1 :
[2649]85  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
86  'a1
[2601]87
88val universe_inv_rect_Type0 :
[2649]89  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
90  'a1
[2601]91
[2649]92val universe_discr :
93  PreIdentifiers.identifierTag -> universe -> universe -> __
[2601]94
[2649]95val universe_jmdiscr :
96  PreIdentifiers.identifierTag -> universe -> universe -> __
[2601]97
[2649]98val new_universe : PreIdentifiers.identifierTag -> universe
[2601]99
100val fresh :
[2649]101  PreIdentifiers.identifierTag -> universe -> (PreIdentifiers.identifier,
102  universe) Types.prod
[2601]103
104val eq_identifier :
[2649]105  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
106  PreIdentifiers.identifier -> Bool.bool
[2601]107
108val eq_identifier_elim :
[2649]109  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
110  PreIdentifiers.identifier -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
[2601]111
112open Deqsets
113
[2649]114val deq_identifier : PreIdentifiers.identifierTag -> Deqsets.deqSet
[2601]115
116val word_of_identifier :
[2649]117  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> Positive.pos
[2601]118
119val identifier_eq :
[2649]120  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
121  PreIdentifiers.identifier -> (__, __) Types.sum
[2601]122
[2649]123val identifier_of_nat :
124  PreIdentifiers.identifierTag -> Nat.nat -> PreIdentifiers.identifier
[2601]125
126val check_member_env :
[2649]127  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
128  (PreIdentifiers.identifier, 'a1) Types.prod List.list -> __ Errors.res
[2601]129
130val check_distinct_env :
[2649]131  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier, 'a1) Types.prod
132  List.list -> __ Errors.res
[2601]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 :
[2649]141  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
142  'a1 identifier_map -> 'a2
[2601]143
144val identifier_map_rect_Type5 :
[2649]145  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
146  'a1 identifier_map -> 'a2
[2601]147
148val identifier_map_rect_Type3 :
[2649]149  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
150  'a1 identifier_map -> 'a2
[2601]151
152val identifier_map_rect_Type2 :
[2649]153  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
154  'a1 identifier_map -> 'a2
[2601]155
156val identifier_map_rect_Type1 :
[2649]157  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
158  'a1 identifier_map -> 'a2
[2601]159
160val identifier_map_rect_Type0 :
[2649]161  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
162  'a1 identifier_map -> 'a2
[2601]163
164val identifier_map_inv_rect_Type4 :
[2649]165  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
166  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
[2601]167
168val identifier_map_inv_rect_Type3 :
[2649]169  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
170  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
[2601]171
172val identifier_map_inv_rect_Type2 :
[2649]173  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
174  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
[2601]175
176val identifier_map_inv_rect_Type1 :
[2649]177  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
178  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
[2601]179
180val identifier_map_inv_rect_Type0 :
[2649]181  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
182  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
[2601]183
184val identifier_map_discr :
[2649]185  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
186  __
[2601]187
188val identifier_map_jmdiscr :
[2649]189  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
190  __
[2601]191
[2649]192val empty_map : PreIdentifiers.identifierTag -> 'a1 identifier_map
[2601]193
[2773]194val lookup :
[2649]195  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
196  PreIdentifiers.identifier -> 'a1 Types.option
[2601]197
198val lookup_def :
[2649]199  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
200  PreIdentifiers.identifier -> 'a1 -> 'a1
[2601]201
[2773]202val member :
[2649]203  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
204  PreIdentifiers.identifier -> Bool.bool
[2601]205
206val lookup_safe :
[2649]207  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
208  PreIdentifiers.identifier -> 'a1
[2601]209
210val add :
[2649]211  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
212  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map
[2601]213
214val elements :
[2649]215  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
216  (PreIdentifiers.identifier, 'a1) Types.prod List.list
[2601]217
218val idmap_all :
[2649]219  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
220  (PreIdentifiers.identifier -> 'a1 -> __ -> Bool.bool) -> Bool.bool
[2601]221
[2773]222val update :
[2649]223  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
224  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map Errors.res
[2601]225
226val remove :
[2649]227  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
228  PreIdentifiers.identifier -> 'a1 identifier_map
[2601]229
[2773]230val foldi :
[2649]231  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> 'a1 -> 'a2 ->
232  'a2) -> 'a1 identifier_map -> 'a2 -> 'a2
[2601]233
234val fold_inf :
[2649]235  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
236  (PreIdentifiers.identifier -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2
[2601]237
[2773]238val find :
[2649]239  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
240  (PreIdentifiers.identifier -> 'a1 -> Bool.bool) ->
241  (PreIdentifiers.identifier, 'a1) Types.prod Types.option
[2601]242
243val lookup_present :
[2649]244  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
245  PreIdentifiers.identifier -> 'a1
[2601]246
247val update_present :
[2649]248  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
249  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map
[2601]250
251type identifier_set = Types.unit0 identifier_map
252
[2649]253val empty_set : PreIdentifiers.identifierTag -> identifier_set
[2601]254
255val add_set :
[2649]256  PreIdentifiers.identifierTag -> identifier_set -> PreIdentifiers.identifier
257  -> identifier_set
[2601]258
259val singleton_set :
[2649]260  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier_set
[2601]261
262val union_set :
[2649]263  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
264  identifier_set
[2601]265
266val minus_set :
[2649]267  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
268  'a1 identifier_map
[2601]269
[2649]270val identifierSet : PreIdentifiers.identifierTag -> Setoids.setoid
[2601]271
[2649]272val id_map_size :
273  PreIdentifiers.identifierTag -> 'a1 identifier_map -> Nat.nat
[2601]274
275open Proper
276
277val set_from_list :
[2649]278  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
279  Types.unit0 identifier_map
[2601]280
[2743]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
[2601]301val choose :
[2649]302  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
303  ((PreIdentifiers.identifier, 'a1) Types.prod, 'a1 identifier_map)
304  Types.prod Types.option
[2601]305
306val try_remove :
[2649]307  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
308  PreIdentifiers.identifier -> ('a1, 'a1 identifier_map) Types.prod
309  Types.option
[2601]310
[2649]311val id_set_of_map :
312  PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set
[2601]313
314val set_of_list :
[2649]315  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
316  identifier_set
[2601]317
[2649]318val domain_of_map :
319  PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set
[2601]320
Note: See TracBrowser for help on using the repository browser.