source: extracted/preIdentifiers.mli @ 2746

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

...

File size: 2.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
21type identifierTag =
22| Label
23| CostTag
24| RegisterTag
25| LabelTag
26| SymbolTag
27| ASMTag
28
29val identifierTag_rect_Type4 :
30  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1
31
32val identifierTag_rect_Type5 :
33  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1
34
35val identifierTag_rect_Type3 :
36  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1
37
38val identifierTag_rect_Type2 :
39  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1
40
41val identifierTag_rect_Type1 :
42  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1
43
44val identifierTag_rect_Type0 :
45  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1
46
47val identifierTag_inv_rect_Type4 :
48  identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
49  -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
50
51val identifierTag_inv_rect_Type3 :
52  identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
53  -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
54
55val identifierTag_inv_rect_Type2 :
56  identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
57  -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
58
59val identifierTag_inv_rect_Type1 :
60  identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
61  -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
62
63val identifierTag_inv_rect_Type0 :
64  identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
65  -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
66
67val identifierTag_discr : identifierTag -> identifierTag -> __
68
69type identifier =
70  Positive.pos
71  (* singleton inductive, whose constructor was an_identifier *)
72
73val identifier_rect_Type4 :
74  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
75
76val identifier_rect_Type5 :
77  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
78
79val identifier_rect_Type3 :
80  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
81
82val identifier_rect_Type2 :
83  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
84
85val identifier_rect_Type1 :
86  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
87
88val identifier_rect_Type0 :
89  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
90
91val identifier_inv_rect_Type4 :
92  identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1
93
94val identifier_inv_rect_Type3 :
95  identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1
96
97val identifier_inv_rect_Type2 :
98  identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1
99
100val identifier_inv_rect_Type1 :
101  identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1
102
103val identifier_inv_rect_Type0 :
104  identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1
105
106val identifier_discr : identifierTag -> identifier -> identifier -> __
107
Note: See TracBrowser for help on using the repository browser.