source: extracted/preIdentifiers.mli @ 3009

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

...

File size: 2.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
[2649]19open Positive
[2601]20
[2649]21type identifierTag =
22| Label
23| CostTag
24| RegisterTag
25| LabelTag
26| SymbolTag
27| ASMTag
[2601]28
[2649]29val identifierTag_rect_Type4 :
30  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1
[2601]31
[2649]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
[2601]69type identifier =
70  Positive.pos
71  (* singleton inductive, whose constructor was an_identifier *)
72
73val identifier_rect_Type4 :
[2649]74  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
[2601]75
76val identifier_rect_Type5 :
[2649]77  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
[2601]78
79val identifier_rect_Type3 :
[2649]80  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
[2601]81
82val identifier_rect_Type2 :
[2649]83  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
[2601]84
85val identifier_rect_Type1 :
[2649]86  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
[2601]87
88val identifier_rect_Type0 :
[2649]89  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
[2601]90
91val identifier_inv_rect_Type4 :
[2649]92  identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1
[2601]93
94val identifier_inv_rect_Type3 :
[2649]95  identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1
[2601]96
97val identifier_inv_rect_Type2 :
[2649]98  identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1
[2601]99
100val identifier_inv_rect_Type1 :
[2649]101  identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1
[2601]102
103val identifier_inv_rect_Type0 :
[2649]104  identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1
[2601]105
[2649]106val identifier_discr : identifierTag -> identifier -> identifier -> __
[2601]107
Note: See TracBrowser for help on using the repository browser.