source: driver/extracted/bigops.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: 5.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 Div_and_mod
20
21val prodF :
22  (Nat.nat -> 'a1) -> (Nat.nat -> 'a2) -> Nat.nat -> Nat.nat -> ('a1, 'a2)
23  Types.prod
24
25val bigop :
26  Nat.nat -> (Nat.nat -> Bool.bool) -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> (Nat.nat
27  -> 'a1) -> 'a1
28
29type 'a aop =
30  'a -> 'a -> 'a
31  (* singleton inductive, whose constructor was mk_Aop *)
32
33val aop_rect_Type4 :
34  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
35
36val aop_rect_Type5 :
37  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
38
39val aop_rect_Type3 :
40  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
41
42val aop_rect_Type2 :
43  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
44
45val aop_rect_Type1 :
46  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
47
48val aop_rect_Type0 :
49  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
50
51val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1
52
53val aop_inv_rect_Type4 :
54  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
55  'a2
56
57val aop_inv_rect_Type3 :
58  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
59  'a2
60
61val aop_inv_rect_Type2 :
62  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
63  'a2
64
65val aop_inv_rect_Type1 :
66  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
67  'a2
68
69val aop_inv_rect_Type0 :
70  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
71  'a2
72
73val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __
74
75val dpi1__o__op : 'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1
76
77type 'a aCop =
78  'a aop
79  (* singleton inductive, whose constructor was mk_ACop *)
80
81val aCop_rect_Type4 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
82
83val aCop_rect_Type5 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
84
85val aCop_rect_Type3 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
86
87val aCop_rect_Type2 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
88
89val aCop_rect_Type1 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
90
91val aCop_rect_Type0 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
92
93val aop0 : 'a1 -> 'a1 aCop -> 'a1 aop
94
95val aCop_inv_rect_Type4 :
96  'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2
97
98val aCop_inv_rect_Type3 :
99  'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2
100
101val aCop_inv_rect_Type2 :
102  'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2
103
104val aCop_inv_rect_Type1 :
105  'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2
106
107val aCop_inv_rect_Type0 :
108  'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2
109
110val aCop_discr : 'a1 -> 'a1 aCop -> 'a1 aCop -> __
111
112val dpi1__o__aop__o__op :
113  'a1 -> ('a1 aCop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1
114
115val aop__o__op : 'a1 -> 'a1 aCop -> 'a1 -> 'a1 -> 'a1
116
117val dpi1__o__aop : 'a1 -> ('a1 aCop, 'a2) Types.dPair -> 'a1 aop
118
119type 'a range = { enum : (Nat.nat -> 'a); upto : Nat.nat;
120                  filter : (Nat.nat -> Bool.bool) }
121
122val range_rect_Type4 :
123  ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
124  -> 'a2
125
126val range_rect_Type5 :
127  ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
128  -> 'a2
129
130val range_rect_Type3 :
131  ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
132  -> 'a2
133
134val range_rect_Type2 :
135  ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
136  -> 'a2
137
138val range_rect_Type1 :
139  ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
140  -> 'a2
141
142val range_rect_Type0 :
143  ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
144  -> 'a2
145
146val enum : 'a1 range -> Nat.nat -> 'a1
147
148val upto : 'a1 range -> Nat.nat
149
150val filter : 'a1 range -> Nat.nat -> Bool.bool
151
152val range_inv_rect_Type4 :
153  'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
154  -> 'a2) -> 'a2
155
156val range_inv_rect_Type3 :
157  'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
158  -> 'a2) -> 'a2
159
160val range_inv_rect_Type2 :
161  'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
162  -> 'a2) -> 'a2
163
164val range_inv_rect_Type1 :
165  'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
166  -> 'a2) -> 'a2
167
168val range_inv_rect_Type0 :
169  'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
170  -> 'a2) -> 'a2
171
172val range_discr : 'a1 range -> 'a1 range -> __
173
174type 'a dop = { sum0 : 'a aCop; prod0 : ('a -> 'a -> 'a) }
175
176val dop_rect_Type4 :
177  'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
178  'a2
179
180val dop_rect_Type5 :
181  'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
182  'a2
183
184val dop_rect_Type3 :
185  'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
186  'a2
187
188val dop_rect_Type2 :
189  'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
190  'a2
191
192val dop_rect_Type1 :
193  'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
194  'a2
195
196val dop_rect_Type0 :
197  'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
198  'a2
199
200val sum0 : 'a1 -> 'a1 dop -> 'a1 aCop
201
202val prod0 : 'a1 -> 'a1 dop -> 'a1 -> 'a1 -> 'a1
203
204val dop_inv_rect_Type4 :
205  'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
206  'a2) -> 'a2
207
208val dop_inv_rect_Type3 :
209  'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
210  'a2) -> 'a2
211
212val dop_inv_rect_Type2 :
213  'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
214  'a2) -> 'a2
215
216val dop_inv_rect_Type1 :
217  'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
218  'a2) -> 'a2
219
220val dop_inv_rect_Type0 :
221  'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
222  'a2) -> 'a2
223
224val dop_discr : 'a1 -> 'a1 dop -> 'a1 dop -> __
225
Note: See TracBrowser for help on using the repository browser.