source: extracted/monad.mli @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

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_1762 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_1762 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
145type 'a sm_eq = __
146
147val setoidMonadProps_inv_rect_Type4 :
148  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
149  -> __ -> __ -> 'a1) -> 'a1
150
151val setoidMonadProps_inv_rect_Type3 :
152  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
153  -> __ -> __ -> 'a1) -> 'a1
154
155val setoidMonadProps_inv_rect_Type2 :
156  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
157  -> __ -> __ -> 'a1) -> 'a1
158
159val setoidMonadProps_inv_rect_Type1 :
160  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
161  -> __ -> __ -> 'a1) -> 'a1
162
163val setoidMonadProps_inv_rect_Type0 :
164  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
165  -> __ -> __ -> 'a1) -> 'a1
166
167type 'x_1762 smax_def__o__monad = __
168
169val setoid_of_monad : setoidMonadProps -> Setoids.setoid
170
171open Bool
172
173open Nat
174
175open List
176
177val m_map : monad -> ('a1 -> 'a2) -> __ -> __
178
179val m_map2 : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __
180
181val m_bind2 : monad -> __ -> ('a1 -> 'a2 -> __) -> __
182
183val m_bind3 : monad -> __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __
184
185val m_join : monad -> __ -> __
186
187val m_sigbind2 : monad -> __ -> ('a1 -> 'a2 -> __ -> __) -> __
188
189val m_list_map : monad -> ('a1 -> __) -> 'a1 List.list -> __
190
191val m_list_map_sigma : monad -> ('a1 -> __) -> 'a1 List.list -> __
192
193val m_bin_op : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __
194
195val m_fold : monad -> ('a1 -> 'a2 -> __) -> 'a1 List.list -> 'a2 -> __
196
197val makeMonadProps :
198  (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) -> monadProps
199
200val makeSetoidMonadProps :
201  (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) ->
202  setoidMonadProps
203
204open Jmeq
205
206open Russell
207
208type monadPred =
209| Mk_MonadPred
210
211val monadPred_rect_Type4 :
212  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
213
214val monadPred_rect_Type5 :
215  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
216
217val monadPred_rect_Type3 :
218  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
219
220val monadPred_rect_Type2 :
221  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
222
223val monadPred_rect_Type1 :
224  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
225
226val monadPred_rect_Type0 :
227  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
228
229type 'a m_pred = __
230
231val monadPred_inv_rect_Type4 :
232  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
233
234val monadPred_inv_rect_Type3 :
235  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
236
237val monadPred_inv_rect_Type2 :
238  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
239
240val monadPred_inv_rect_Type1 :
241  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
242
243val monadPred_inv_rect_Type0 :
244  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
245
246val monadPred_jmdiscr : monad -> monadPred -> monadPred -> __
247
248type injMonadPred = { im_pred : monadPred;
249                      mp_inject : (__ -> __ -> __ Types.sig0 -> __) }
250
251val injMonadPred_rect_Type4 :
252  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
253  injMonadPred -> 'a1
254
255val injMonadPred_rect_Type5 :
256  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
257  injMonadPred -> 'a1
258
259val injMonadPred_rect_Type3 :
260  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
261  injMonadPred -> 'a1
262
263val injMonadPred_rect_Type2 :
264  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
265  injMonadPred -> 'a1
266
267val injMonadPred_rect_Type1 :
268  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
269  injMonadPred -> 'a1
270
271val injMonadPred_rect_Type0 :
272  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
273  injMonadPred -> 'a1
274
275val im_pred : monad -> injMonadPred -> monadPred
276
277val mp_inject0 : monad -> injMonadPred -> __ Types.sig0 -> __
278
279val injMonadPred_inv_rect_Type4 :
280  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
281  __ -> __ -> 'a1) -> 'a1
282
283val injMonadPred_inv_rect_Type3 :
284  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
285  __ -> __ -> 'a1) -> 'a1
286
287val injMonadPred_inv_rect_Type2 :
288  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
289  __ -> __ -> 'a1) -> 'a1
290
291val injMonadPred_inv_rect_Type1 :
292  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
293  __ -> __ -> 'a1) -> 'a1
294
295val injMonadPred_inv_rect_Type0 :
296  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
297  __ -> __ -> 'a1) -> 'a1
298
299val injMonadPred_jmdiscr : monad -> injMonadPred -> injMonadPred -> __
300
301type monadRel =
302| Mk_MonadRel
303
304val monadRel_rect_Type4 :
305  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
306
307val monadRel_rect_Type5 :
308  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
309
310val monadRel_rect_Type3 :
311  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
312
313val monadRel_rect_Type2 :
314  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
315
316val monadRel_rect_Type1 :
317  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
318
319val monadRel_rect_Type0 :
320  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
321
322type ('a,'b) m_rel = __
323
324val monadRel_inv_rect_Type4 :
325  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
326
327val monadRel_inv_rect_Type3 :
328  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
329
330val monadRel_inv_rect_Type2 :
331  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
332
333val monadRel_inv_rect_Type1 :
334  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
335
336val monadRel_inv_rect_Type0 :
337  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
338
339val monadRel_jmdiscr : monad -> monad -> monadRel -> monadRel -> __
340
Note: See TracBrowser for help on using the repository browser.