source: extracted/monad.mli @ 2773

Last change on this file since 2773 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: 9.5 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Relations
14
15open Setoids
16
17type ('a, 'b) pred_transformer = __
18
19type ('a, 'b, 'c, 'd) rel_transformer = __
20
21type monad = { m_return : (__ -> __ -> __);
22               m_bind : (__ -> __ -> __ -> (__ -> __) -> __) }
23
24val monad_rect_Type4 :
25  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
26  monad -> 'a1
27
28val monad_rect_Type5 :
29  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
30  monad -> 'a1
31
32val monad_rect_Type3 :
33  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
34  monad -> 'a1
35
36val monad_rect_Type2 :
37  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
38  monad -> 'a1
39
40val monad_rect_Type1 :
41  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
42  monad -> 'a1
43
44val monad_rect_Type0 :
45  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
46  monad -> 'a1
47
48type 'x_1502 monad0
49
50val m_return0 : monad -> 'a1 -> __
51
52val m_bind0 : monad -> __ -> ('a1 -> __) -> __
53
54val monad_inv_rect_Type4 :
55  monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
56  __ -> 'a1) -> 'a1
57
58val monad_inv_rect_Type3 :
59  monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
60  __ -> 'a1) -> 'a1
61
62val monad_inv_rect_Type2 :
63  monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
64  __ -> 'a1) -> 'a1
65
66val monad_inv_rect_Type1 :
67  monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
68  __ -> 'a1) -> 'a1
69
70val monad_inv_rect_Type0 :
71  monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
72  __ -> 'a1) -> 'a1
73
74type monadProps =
75  monad
76  (* singleton inductive, whose constructor was mk_MonadProps *)
77
78val monadProps_rect_Type4 :
79  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
80
81val monadProps_rect_Type5 :
82  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
83
84val monadProps_rect_Type3 :
85  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
86
87val monadProps_rect_Type2 :
88  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
89
90val monadProps_rect_Type1 :
91  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
92
93val monadProps_rect_Type0 :
94  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
95
96val max_def : monadProps -> monad
97
98val monadProps_inv_rect_Type4 :
99  monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
100
101val monadProps_inv_rect_Type3 :
102  monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
103
104val monadProps_inv_rect_Type2 :
105  monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
106
107val monadProps_inv_rect_Type1 :
108  monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
109
110val monadProps_inv_rect_Type0 :
111  monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
112
113type 'x_1502 max_def__o__monad = __
114
115type setoidMonadProps =
116  monad
117  (* singleton inductive, whose constructor was mk_SetoidMonadProps *)
118
119val setoidMonadProps_rect_Type4 :
120  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
121  setoidMonadProps -> 'a1
122
123val setoidMonadProps_rect_Type5 :
124  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
125  setoidMonadProps -> 'a1
126
127val setoidMonadProps_rect_Type3 :
128  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
129  setoidMonadProps -> 'a1
130
131val setoidMonadProps_rect_Type2 :
132  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
133  setoidMonadProps -> 'a1
134
135val setoidMonadProps_rect_Type1 :
136  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
137  setoidMonadProps -> 'a1
138
139val setoidMonadProps_rect_Type0 :
140  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
141  setoidMonadProps -> 'a1
142
143val smax_def : setoidMonadProps -> monad
144
145val setoidMonadProps_inv_rect_Type4 :
146  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
147  -> __ -> __ -> 'a1) -> 'a1
148
149val setoidMonadProps_inv_rect_Type3 :
150  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
151  -> __ -> __ -> 'a1) -> 'a1
152
153val setoidMonadProps_inv_rect_Type2 :
154  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
155  -> __ -> __ -> 'a1) -> 'a1
156
157val setoidMonadProps_inv_rect_Type1 :
158  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
159  -> __ -> __ -> 'a1) -> 'a1
160
161val setoidMonadProps_inv_rect_Type0 :
162  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
163  -> __ -> __ -> 'a1) -> 'a1
164
165type 'x_1502 smax_def__o__monad = __
166
167val setoid_of_monad : setoidMonadProps -> Setoids.setoid
168
169open Bool
170
171open Nat
172
173open List
174
175val m_map : monad -> ('a1 -> 'a2) -> __ -> __
176
177val m_map2 : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __
178
179val m_bind2 : monad -> __ -> ('a1 -> 'a2 -> __) -> __
180
181val m_bind3 : monad -> __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __
182
183val m_join : monad -> __ -> __
184
185val m_sigbind2 : monad -> __ -> ('a1 -> 'a2 -> __ -> __) -> __
186
187val m_list_map : monad -> ('a1 -> __) -> 'a1 List.list -> __
188
189val m_list_map_sigma : monad -> ('a1 -> __) -> 'a1 List.list -> __
190
191val m_bin_op : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __
192
193val m_fold : monad -> ('a1 -> 'a2 -> __) -> 'a1 List.list -> 'a2 -> __
194
195val makeMonadProps :
196  (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) -> monadProps
197
198val makeSetoidMonadProps :
199  (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) ->
200  setoidMonadProps
201
202open Jmeq
203
204open Russell
205
206type monadPred =
207| Mk_MonadPred
208
209val monadPred_rect_Type4 :
210  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
211
212val monadPred_rect_Type5 :
213  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
214
215val monadPred_rect_Type3 :
216  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
217
218val monadPred_rect_Type2 :
219  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
220
221val monadPred_rect_Type1 :
222  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
223
224val monadPred_rect_Type0 :
225  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
226
227val monadPred_inv_rect_Type4 :
228  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
229
230val monadPred_inv_rect_Type3 :
231  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
232
233val monadPred_inv_rect_Type2 :
234  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
235
236val monadPred_inv_rect_Type1 :
237  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
238
239val monadPred_inv_rect_Type0 :
240  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
241
242val monadPred_jmdiscr : monad -> monadPred -> monadPred -> __
243
244type injMonadPred = { im_pred : monadPred;
245                      mp_inject : (__ -> __ -> __ Types.sig0 -> __) }
246
247val injMonadPred_rect_Type4 :
248  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
249  injMonadPred -> 'a1
250
251val injMonadPred_rect_Type5 :
252  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
253  injMonadPred -> 'a1
254
255val injMonadPred_rect_Type3 :
256  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
257  injMonadPred -> 'a1
258
259val injMonadPred_rect_Type2 :
260  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
261  injMonadPred -> 'a1
262
263val injMonadPred_rect_Type1 :
264  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
265  injMonadPred -> 'a1
266
267val injMonadPred_rect_Type0 :
268  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
269  injMonadPred -> 'a1
270
271val im_pred : monad -> injMonadPred -> monadPred
272
273val mp_inject0 : monad -> injMonadPred -> __ Types.sig0 -> __
274
275val injMonadPred_inv_rect_Type4 :
276  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
277  __ -> __ -> 'a1) -> 'a1
278
279val injMonadPred_inv_rect_Type3 :
280  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
281  __ -> __ -> 'a1) -> 'a1
282
283val injMonadPred_inv_rect_Type2 :
284  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
285  __ -> __ -> 'a1) -> 'a1
286
287val injMonadPred_inv_rect_Type1 :
288  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
289  __ -> __ -> 'a1) -> 'a1
290
291val injMonadPred_inv_rect_Type0 :
292  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
293  __ -> __ -> 'a1) -> 'a1
294
295val injMonadPred_jmdiscr : monad -> injMonadPred -> injMonadPred -> __
296
297type monadRel =
298| Mk_MonadRel
299
300val monadRel_rect_Type4 :
301  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
302
303val monadRel_rect_Type5 :
304  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
305
306val monadRel_rect_Type3 :
307  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
308
309val monadRel_rect_Type2 :
310  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
311
312val monadRel_rect_Type1 :
313  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
314
315val monadRel_rect_Type0 :
316  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
317
318val monadRel_inv_rect_Type4 :
319  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
320
321val monadRel_inv_rect_Type3 :
322  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
323
324val monadRel_inv_rect_Type2 :
325  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
326
327val monadRel_inv_rect_Type1 :
328  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
329
330val monadRel_inv_rect_Type0 :
331  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
332
333val monadRel_jmdiscr : monad -> monad -> monadRel -> monadRel -> __
334
Note: See TracBrowser for help on using the repository browser.