source: extracted/identifiers.mli @ 2716

Last change on this file since 2716 was 2649, checked in by sacerdot, 7 years ago

...

File size: 8.2 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
104type fresh_for_univ = __
105
106type env_fresh_for_univ = __
107
108val eq_identifier :
[2649]109  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
110  PreIdentifiers.identifier -> Bool.bool
[2601]111
112val eq_identifier_elim :
[2649]113  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
114  PreIdentifiers.identifier -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
[2601]115
116open Deqsets
117
[2649]118val deq_identifier : PreIdentifiers.identifierTag -> Deqsets.deqSet
[2601]119
120val word_of_identifier :
[2649]121  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> Positive.pos
[2601]122
123val identifier_eq :
[2649]124  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
125  PreIdentifiers.identifier -> (__, __) Types.sum
[2601]126
[2649]127val identifier_of_nat :
128  PreIdentifiers.identifierTag -> Nat.nat -> PreIdentifiers.identifier
[2601]129
130type distinct_env = __
131
132val check_member_env :
[2649]133  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
134  (PreIdentifiers.identifier, 'a1) Types.prod List.list -> __ Errors.res
[2601]135
136val check_distinct_env :
[2649]137  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier, 'a1) Types.prod
138  List.list -> __ Errors.res
[2601]139
140open PositiveMap
141
142type 'a identifier_map =
143  'a PositiveMap.positive_map
144  (* singleton inductive, whose constructor was an_id_map *)
145
146val identifier_map_rect_Type4 :
[2649]147  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
148  'a1 identifier_map -> 'a2
[2601]149
150val identifier_map_rect_Type5 :
[2649]151  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
152  'a1 identifier_map -> 'a2
[2601]153
154val identifier_map_rect_Type3 :
[2649]155  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
156  'a1 identifier_map -> 'a2
[2601]157
158val identifier_map_rect_Type2 :
[2649]159  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
160  'a1 identifier_map -> 'a2
[2601]161
162val identifier_map_rect_Type1 :
[2649]163  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
164  'a1 identifier_map -> 'a2
[2601]165
166val identifier_map_rect_Type0 :
[2649]167  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
168  'a1 identifier_map -> 'a2
[2601]169
170val identifier_map_inv_rect_Type4 :
[2649]171  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
172  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
[2601]173
174val identifier_map_inv_rect_Type3 :
[2649]175  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
176  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
[2601]177
178val identifier_map_inv_rect_Type2 :
[2649]179  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
180  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
[2601]181
182val identifier_map_inv_rect_Type1 :
[2649]183  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
184  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
[2601]185
186val identifier_map_inv_rect_Type0 :
[2649]187  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
188  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
[2601]189
190val identifier_map_discr :
[2649]191  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
192  __
[2601]193
194val identifier_map_jmdiscr :
[2649]195  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
196  __
[2601]197
[2649]198val empty_map : PreIdentifiers.identifierTag -> 'a1 identifier_map
[2601]199
200val lookup0 :
[2649]201  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
202  PreIdentifiers.identifier -> 'a1 Types.option
[2601]203
204val lookup_def :
[2649]205  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
206  PreIdentifiers.identifier -> 'a1 -> 'a1
[2601]207
208val member0 :
[2649]209  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
210  PreIdentifiers.identifier -> Bool.bool
[2601]211
212val lookup_safe :
[2649]213  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
214  PreIdentifiers.identifier -> 'a1
[2601]215
216val add :
[2649]217  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
218  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map
[2601]219
220val elements :
[2649]221  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
222  (PreIdentifiers.identifier, 'a1) Types.prod List.list
[2601]223
224val idmap_all :
[2649]225  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
226  (PreIdentifiers.identifier -> 'a1 -> __ -> Bool.bool) -> Bool.bool
[2601]227
228val update0 :
[2649]229  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
230  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map Errors.res
[2601]231
232val remove :
[2649]233  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
234  PreIdentifiers.identifier -> 'a1 identifier_map
[2601]235
236val foldi0 :
[2649]237  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> 'a1 -> 'a2 ->
238  'a2) -> 'a1 identifier_map -> 'a2 -> 'a2
[2601]239
240val fold_inf :
[2649]241  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
242  (PreIdentifiers.identifier -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2
[2601]243
244val find0 :
[2649]245  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
246  (PreIdentifiers.identifier -> 'a1 -> Bool.bool) ->
247  (PreIdentifiers.identifier, 'a1) Types.prod Types.option
[2601]248
249val lookup_present :
[2649]250  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
251  PreIdentifiers.identifier -> 'a1
[2601]252
253val update_present :
[2649]254  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
255  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map
[2601]256
257type fresh_for_map = __
258
259type identifier_set = Types.unit0 identifier_map
260
[2649]261val empty_set : PreIdentifiers.identifierTag -> identifier_set
[2601]262
263val add_set :
[2649]264  PreIdentifiers.identifierTag -> identifier_set -> PreIdentifiers.identifier
265  -> identifier_set
[2601]266
267val singleton_set :
[2649]268  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier_set
[2601]269
270val union_set :
[2649]271  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
272  identifier_set
[2601]273
274val minus_set :
[2649]275  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
276  'a1 identifier_map
[2601]277
[2649]278val identifierSet : PreIdentifiers.identifierTag -> Setoids.setoid
[2601]279
[2649]280val id_map_size :
281  PreIdentifiers.identifierTag -> 'a1 identifier_map -> Nat.nat
[2601]282
283open Proper
284
285val set_from_list :
[2649]286  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
287  Types.unit0 identifier_map
[2601]288
289val choose :
[2649]290  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
291  ((PreIdentifiers.identifier, 'a1) Types.prod, 'a1 identifier_map)
292  Types.prod Types.option
[2601]293
294val try_remove :
[2649]295  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
296  PreIdentifiers.identifier -> ('a1, 'a1 identifier_map) Types.prod
297  Types.option
[2601]298
[2649]299val id_set_of_map :
300  PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set
[2601]301
302val set_of_list :
[2649]303  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
304  identifier_set
[2601]305
[2649]306val domain_of_map :
307  PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set
[2601]308
Note: See TracBrowser for help on using the repository browser.