source: driver/extracted/positive.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 3.8 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Bool
12
13open Relations
14
15open Nat
16
17type compare =
18| LT
19| EQ
20| GT
21
22val compare_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
23
24val compare_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
25
26val compare_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
27
28val compare_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
29
30val compare_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
31
32val compare_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
33
34val compare_inv_rect_Type4 :
35  compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
36
37val compare_inv_rect_Type3 :
38  compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
39
40val compare_inv_rect_Type2 :
41  compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
42
43val compare_inv_rect_Type1 :
44  compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
45
46val compare_inv_rect_Type0 :
47  compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
48
49val compare_discr : compare -> compare -> __
50
51val compare_invert : compare -> compare
52
53type pos =
54| One
55| P1 of pos
56| P0 of pos
57
58val pos_rect_Type4 :
59  'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1
60
61val pos_rect_Type3 :
62  'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1
63
64val pos_rect_Type2 :
65  'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1
66
67val pos_rect_Type1 :
68  'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1
69
70val pos_rect_Type0 :
71  'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1
72
73val pos_inv_rect_Type4 :
74  pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
75  'a1) -> __ -> 'a1) -> 'a1
76
77val pos_inv_rect_Type3 :
78  pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
79  'a1) -> __ -> 'a1) -> 'a1
80
81val pos_inv_rect_Type2 :
82  pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
83  'a1) -> __ -> 'a1) -> 'a1
84
85val pos_inv_rect_Type1 :
86  pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
87  'a1) -> __ -> 'a1) -> 'a1
88
89val pos_inv_rect_Type0 :
90  pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
91  'a1) -> __ -> 'a1) -> 'a1
92
93val pos_discr : pos -> pos -> __
94
95val pred : pos -> pos
96
97val succ : pos -> pos
98
99val nat_of_pos : pos -> Nat.nat
100
101val succ_pos_of_nat : Nat.nat -> pos
102
103val plus : pos -> pos -> pos
104
105val times : pos -> pos -> pos
106
107type minusresult =
108| MinusNeg
109| MinusZero
110| MinusPos of pos
111
112val minusresult_rect_Type4 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
113
114val minusresult_rect_Type5 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
115
116val minusresult_rect_Type3 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
117
118val minusresult_rect_Type2 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
119
120val minusresult_rect_Type1 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
121
122val minusresult_rect_Type0 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
123
124val minusresult_inv_rect_Type4 :
125  minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1
126
127val minusresult_inv_rect_Type3 :
128  minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1
129
130val minusresult_inv_rect_Type2 :
131  minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1
132
133val minusresult_inv_rect_Type1 :
134  minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1
135
136val minusresult_inv_rect_Type0 :
137  minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1
138
139val minusresult_discr : minusresult -> minusresult -> __
140
141val partial_minus : pos -> pos -> minusresult
142
143val minus : pos -> pos -> pos
144
145val eqb : pos -> pos -> Bool.bool
146
147val eqb_elim : pos -> pos -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
148
149val leb : pos -> pos -> Bool.bool
150
151val pos_compare : pos -> pos -> compare
152
153val two_power_nat : Nat.nat -> pos
154
155val two_power_pos : pos -> pos
156
157val max : pos -> pos -> pos
158
Note: See TracBrowser for help on using the repository browser.