49 (* singleton inductive, whose constructor was mk_universe *)
51 val universe_rect_Type4 :
52 PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
54 val universe_rect_Type5 :
55 PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
57 val universe_rect_Type3 :
58 PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
60 val universe_rect_Type2 :
61 PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
63 val universe_rect_Type1 :
64 PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
66 val universe_rect_Type0 :
67 PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
70 PreIdentifiers.identifierTag -> universe -> Positive.pos
72 val universe_inv_rect_Type4 :
73 PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
76 val universe_inv_rect_Type3 :
77 PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
80 val universe_inv_rect_Type2 :
81 PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
84 val universe_inv_rect_Type1 :
85 PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
88 val universe_inv_rect_Type0 :
89 PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
93 PreIdentifiers.identifierTag -> universe -> universe -> __
95 val universe_jmdiscr :
96 PreIdentifiers.identifierTag -> universe -> universe -> __
98 val new_universe : PreIdentifiers.identifierTag -> universe
101 PreIdentifiers.identifierTag -> universe -> (PreIdentifiers.identifier,
105 PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
106 PreIdentifiers.identifier -> Bool.bool
108 val eq_identifier_elim :
109 PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
110 PreIdentifiers.identifier -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
114 val deq_identifier : PreIdentifiers.identifierTag -> Deqsets.deqSet
116 val word_of_identifier :
117 PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> Positive.pos
120 PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
121 PreIdentifiers.identifier -> (__, __) Types.sum
123 val identifier_of_nat :
124 PreIdentifiers.identifierTag -> Nat.nat -> PreIdentifiers.identifier
126 val check_member_env :
127 PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
128 (PreIdentifiers.identifier, 'a1) Types.prod List.list -> __ Errors.res
130 val check_distinct_env :
131 PreIdentifiers.identifierTag -> (PreIdentifiers.identifier, 'a1) Types.prod
132 List.list -> __ Errors.res
136 type 'a identifier_map =
137 'a PositiveMap.positive_map
138 (* singleton inductive, whose constructor was an_id_map *)
140 val identifier_map_rect_Type4 :
141 PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
142 'a1 identifier_map -> 'a2
144 val identifier_map_rect_Type5 :
145 PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
146 'a1 identifier_map -> 'a2
148 val identifier_map_rect_Type3 :
149 PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
150 'a1 identifier_map -> 'a2
152 val identifier_map_rect_Type2 :
153 PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
154 'a1 identifier_map -> 'a2
156 val identifier_map_rect_Type1 :
157 PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
158 'a1 identifier_map -> 'a2
160 val identifier_map_rect_Type0 :
161 PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
162 'a1 identifier_map -> 'a2
164 val identifier_map_inv_rect_Type4 :
165 PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
166 PositiveMap.positive_map -> __ -> 'a2) -> 'a2
168 val identifier_map_inv_rect_Type3 :
169 PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
170 PositiveMap.positive_map -> __ -> 'a2) -> 'a2
172 val identifier_map_inv_rect_Type2 :
173 PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
174 PositiveMap.positive_map -> __ -> 'a2) -> 'a2
176 val identifier_map_inv_rect_Type1 :
177 PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
178 PositiveMap.positive_map -> __ -> 'a2) -> 'a2
180 val identifier_map_inv_rect_Type0 :
181 PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
182 PositiveMap.positive_map -> __ -> 'a2) -> 'a2
184 val identifier_map_discr :
185 PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
188 val identifier_map_jmdiscr :
189 PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
192 val empty_map : PreIdentifiers.identifierTag -> 'a1 identifier_map
195 PreIdentifiers.identifierTag -> 'a1 identifier_map ->
196 PreIdentifiers.identifier -> 'a1 Types.option
199 PreIdentifiers.identifierTag -> 'a1 identifier_map ->
200 PreIdentifiers.identifier -> 'a1 -> 'a1
203 PreIdentifiers.identifierTag -> 'a1 identifier_map ->
204 PreIdentifiers.identifier -> Bool.bool
207 PreIdentifiers.identifierTag -> 'a1 identifier_map ->
208 PreIdentifiers.identifier -> 'a1
211 PreIdentifiers.identifierTag -> 'a1 identifier_map ->
212 PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map
215 PreIdentifiers.identifierTag -> 'a1 identifier_map ->
216 (PreIdentifiers.identifier, 'a1) Types.prod List.list
219 PreIdentifiers.identifierTag -> 'a1 identifier_map ->
220 (PreIdentifiers.identifier -> 'a1 -> __ -> Bool.bool) -> Bool.bool
223 PreIdentifiers.identifierTag -> 'a1 identifier_map ->
224 PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map Errors.res
227 PreIdentifiers.identifierTag -> 'a1 identifier_map ->
228 PreIdentifiers.identifier -> 'a1 identifier_map
231 PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> 'a1 -> 'a2 ->
232 'a2) -> 'a1 identifier_map -> 'a2 -> 'a2
235 PreIdentifiers.identifierTag -> 'a1 identifier_map ->
236 (PreIdentifiers.identifier -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2
239 PreIdentifiers.identifierTag -> 'a1 identifier_map ->
240 (PreIdentifiers.identifier -> 'a1 -> Bool.bool) ->
241 (PreIdentifiers.identifier, 'a1) Types.prod Types.option
244 PreIdentifiers.identifierTag -> 'a1 identifier_map ->
245 PreIdentifiers.identifier -> 'a1
248 PreIdentifiers.identifierTag -> 'a1 identifier_map ->
249 PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map
251 type identifier_set = Types.unit0 identifier_map
253 val empty_set : PreIdentifiers.identifierTag -> identifier_set
256 PreIdentifiers.identifierTag -> identifier_set -> PreIdentifiers.identifier
260 PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier_set
263 PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
267 PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
270 val identifierSet : PreIdentifiers.identifierTag -> Setoids.setoid
273 PreIdentifiers.identifierTag -> 'a1 identifier_map -> Nat.nat
278 PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
279 Types.unit0 identifier_map
281 val 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
285 val eject__o__id_set_from_list__o__inject :
286 PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
287 Types.sig0 -> Types.unit0 identifier_map Types.sig0
289 val id_set_from_list__o__inject :
290 PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
291 Types.unit0 identifier_map Types.sig0
293 val dpi1__o__id_set_from_list :
294 PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list, 'a1)
295 Types.dPair -> Types.unit0 identifier_map
297 val eject__o__id_set_from_list :
298 PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
299 Types.sig0 -> Types.unit0 identifier_map
302 PreIdentifiers.identifierTag -> 'a1 identifier_map ->
303 ((PreIdentifiers.identifier, 'a1) Types.prod, 'a1 identifier_map)
304 Types.prod Types.option
307 PreIdentifiers.identifierTag -> 'a1 identifier_map ->
308 PreIdentifiers.identifier -> ('a1, 'a1 identifier_map) Types.prod
312 PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set
315 PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
319 PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set