source: extracted/classifyOp.mli @ 2649

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

...

File size: 18.0 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Setoids
22
23open Monad
24
25open Option
26
27open Lists
28
29open Positive
30
31open Identifiers
32
33open Arithmetic
34
35open Vector
36
37open Div_and_mod
38
39open Jmeq
40
41open Russell
42
43open List
44
45open Util
46
47open FoldStuff
48
49open BitVector
50
51open Extranat
52
53open Bool
54
55open Relations
56
57open Nat
58
59open Integers
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Types
70
71open AST
72
73open Csyntax
74
75open TypeComparison
76
77val ptr_type : Csyntax.type0 -> Nat.nat Types.option -> Csyntax.type0
78
79type classify_add_cases =
80| Add_case_ii of AST.intsize * AST.signedness
81| Add_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
82   * AST.signedness
83| Add_case_ip of Nat.nat Types.option * AST.intsize * AST.signedness
84   * Csyntax.type0
85| Add_default of Csyntax.type0 * Csyntax.type0
86
87val classify_add_cases_rect_Type4 :
88  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
89  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
90  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
91  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
92  -> classify_add_cases -> 'a1
93
94val classify_add_cases_rect_Type5 :
95  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
96  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
97  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
98  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
99  -> classify_add_cases -> 'a1
100
101val classify_add_cases_rect_Type3 :
102  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
103  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
104  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
105  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
106  -> classify_add_cases -> 'a1
107
108val classify_add_cases_rect_Type2 :
109  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
110  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
111  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
112  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
113  -> classify_add_cases -> 'a1
114
115val classify_add_cases_rect_Type1 :
116  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
117  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
118  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
119  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
120  -> classify_add_cases -> 'a1
121
122val classify_add_cases_rect_Type0 :
123  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
124  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
125  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
126  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
127  -> classify_add_cases -> 'a1
128
129val classify_add_cases_inv_rect_Type4 :
130  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
131  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
132  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
133  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
134  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
135  -> 'a1) -> 'a1
136
137val classify_add_cases_inv_rect_Type3 :
138  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
139  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
140  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
141  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
142  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
143  -> 'a1) -> 'a1
144
145val classify_add_cases_inv_rect_Type2 :
146  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
147  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
148  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
149  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
150  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
151  -> 'a1) -> 'a1
152
153val classify_add_cases_inv_rect_Type1 :
154  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
155  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
156  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
157  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
158  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
159  -> 'a1) -> 'a1
160
161val classify_add_cases_inv_rect_Type0 :
162  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
163  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
164  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
165  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
166  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
167  -> 'a1) -> 'a1
168
169val classify_add_cases_discr :
170  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> classify_add_cases
171  -> __
172
173val classify_add_cases_jmdiscr :
174  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> classify_add_cases
175  -> __
176
177val classify_add : Csyntax.type0 -> Csyntax.type0 -> classify_add_cases
178
179type classify_sub_cases =
180| Sub_case_ii of AST.intsize * AST.signedness
181| Sub_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
182   * AST.signedness
183| Sub_case_pp of Nat.nat Types.option * Nat.nat Types.option * Csyntax.type0
184   * Csyntax.type0
185| Sub_default of Csyntax.type0 * Csyntax.type0
186
187val classify_sub_cases_rect_Type4 :
188  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
189  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
190  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
191  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
192  Csyntax.type0 -> classify_sub_cases -> 'a1
193
194val classify_sub_cases_rect_Type5 :
195  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
196  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
197  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
198  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
199  Csyntax.type0 -> classify_sub_cases -> 'a1
200
201val classify_sub_cases_rect_Type3 :
202  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
203  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
204  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
205  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
206  Csyntax.type0 -> classify_sub_cases -> 'a1
207
208val classify_sub_cases_rect_Type2 :
209  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
210  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
211  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
212  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
213  Csyntax.type0 -> classify_sub_cases -> 'a1
214
215val classify_sub_cases_rect_Type1 :
216  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
217  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
218  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
219  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
220  Csyntax.type0 -> classify_sub_cases -> 'a1
221
222val classify_sub_cases_rect_Type0 :
223  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
224  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
225  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
226  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
227  Csyntax.type0 -> classify_sub_cases -> 'a1
228
229val classify_sub_cases_inv_rect_Type4 :
230  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
231  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
232  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
233  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
234  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
235  -> __ -> __ -> __ -> 'a1) -> 'a1
236
237val classify_sub_cases_inv_rect_Type3 :
238  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
239  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
240  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
241  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
242  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
243  -> __ -> __ -> __ -> 'a1) -> 'a1
244
245val classify_sub_cases_inv_rect_Type2 :
246  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
247  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
248  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
249  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
250  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
251  -> __ -> __ -> __ -> 'a1) -> 'a1
252
253val classify_sub_cases_inv_rect_Type1 :
254  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
255  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
256  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
257  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
258  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
259  -> __ -> __ -> __ -> 'a1) -> 'a1
260
261val classify_sub_cases_inv_rect_Type0 :
262  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
263  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
264  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
265  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
266  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
267  -> __ -> __ -> __ -> 'a1) -> 'a1
268
269val classify_sub_cases_discr :
270  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> classify_sub_cases
271  -> __
272
273val classify_sub_cases_jmdiscr :
274  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> classify_sub_cases
275  -> __
276
277val classify_sub : Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases
278
279type classify_aop_cases =
280| Aop_case_ii of AST.intsize * AST.signedness
281| Aop_default of Csyntax.type0 * Csyntax.type0
282
283val classify_aop_cases_rect_Type4 :
284  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
285  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
286
287val classify_aop_cases_rect_Type5 :
288  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
289  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
290
291val classify_aop_cases_rect_Type3 :
292  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
293  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
294
295val classify_aop_cases_rect_Type2 :
296  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
297  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
298
299val classify_aop_cases_rect_Type1 :
300  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
301  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
302
303val classify_aop_cases_rect_Type0 :
304  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
305  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
306
307val classify_aop_cases_inv_rect_Type4 :
308  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
309  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
310  -> __ -> __ -> __ -> 'a1) -> 'a1
311
312val classify_aop_cases_inv_rect_Type3 :
313  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
314  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
315  -> __ -> __ -> __ -> 'a1) -> 'a1
316
317val classify_aop_cases_inv_rect_Type2 :
318  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
319  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
320  -> __ -> __ -> __ -> 'a1) -> 'a1
321
322val classify_aop_cases_inv_rect_Type1 :
323  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
324  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
325  -> __ -> __ -> __ -> 'a1) -> 'a1
326
327val classify_aop_cases_inv_rect_Type0 :
328  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
329  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
330  -> __ -> __ -> __ -> 'a1) -> 'a1
331
332val classify_aop_cases_discr :
333  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> classify_aop_cases
334  -> __
335
336val classify_aop_cases_jmdiscr :
337  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> classify_aop_cases
338  -> __
339
340val classify_aop : Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases
341
342type classify_cmp_cases =
343| Cmp_case_ii of AST.intsize * AST.signedness
344| Cmp_case_pp of Nat.nat Types.option * Csyntax.type0
345| Cmp_default of Csyntax.type0 * Csyntax.type0
346
347val classify_cmp_cases_rect_Type4 :
348  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
349  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
350  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
351
352val classify_cmp_cases_rect_Type5 :
353  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
354  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
355  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
356
357val classify_cmp_cases_rect_Type3 :
358  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
359  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
360  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
361
362val classify_cmp_cases_rect_Type2 :
363  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
364  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
365  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
366
367val classify_cmp_cases_rect_Type1 :
368  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
369  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
370  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
371
372val classify_cmp_cases_rect_Type0 :
373  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
374  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
375  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
376
377val classify_cmp_cases_inv_rect_Type4 :
378  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
379  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
380  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
381  -> __ -> __ -> __ -> 'a1) -> 'a1
382
383val classify_cmp_cases_inv_rect_Type3 :
384  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
385  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
386  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
387  -> __ -> __ -> __ -> 'a1) -> 'a1
388
389val classify_cmp_cases_inv_rect_Type2 :
390  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
391  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
392  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
393  -> __ -> __ -> __ -> 'a1) -> 'a1
394
395val classify_cmp_cases_inv_rect_Type1 :
396  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
397  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
398  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
399  -> __ -> __ -> __ -> 'a1) -> 'a1
400
401val classify_cmp_cases_inv_rect_Type0 :
402  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
403  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
404  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
405  -> __ -> __ -> __ -> 'a1) -> 'a1
406
407val classify_cmp_cases_discr :
408  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> classify_cmp_cases
409  -> __
410
411val classify_cmp_cases_jmdiscr :
412  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> classify_cmp_cases
413  -> __
414
415val classify_cmp : Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases
416
417type classify_fun_cases =
418| Fun_case_f of Csyntax.typelist * Csyntax.type0
419| Fun_default
420
421val classify_fun_cases_rect_Type4 :
422  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
423  'a1
424
425val classify_fun_cases_rect_Type5 :
426  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
427  'a1
428
429val classify_fun_cases_rect_Type3 :
430  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
431  'a1
432
433val classify_fun_cases_rect_Type2 :
434  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
435  'a1
436
437val classify_fun_cases_rect_Type1 :
438  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
439  'a1
440
441val classify_fun_cases_rect_Type0 :
442  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
443  'a1
444
445val classify_fun_cases_inv_rect_Type4 :
446  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
447  (__ -> 'a1) -> 'a1
448
449val classify_fun_cases_inv_rect_Type3 :
450  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
451  (__ -> 'a1) -> 'a1
452
453val classify_fun_cases_inv_rect_Type2 :
454  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
455  (__ -> 'a1) -> 'a1
456
457val classify_fun_cases_inv_rect_Type1 :
458  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
459  (__ -> 'a1) -> 'a1
460
461val classify_fun_cases_inv_rect_Type0 :
462  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
463  (__ -> 'a1) -> 'a1
464
465val classify_fun_cases_discr : classify_fun_cases -> classify_fun_cases -> __
466
467val classify_fun_cases_jmdiscr :
468  classify_fun_cases -> classify_fun_cases -> __
469
470val classify_fun : Csyntax.type0 -> classify_fun_cases
471
Note: See TracBrowser for help on using the repository browser.