source: extracted/monad.ml @ 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: 20.2 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
24(** val monad_rect_Type4 :
25    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
26    -> monad -> 'a1 **)
27let rec monad_rect_Type4 h_mk_Monad x_1734 =
28  let { m_return = m_return0; m_bind = m_bind0 } = x_1734 in
29  h_mk_Monad __ m_return0 m_bind0
30
31(** val monad_rect_Type5 :
32    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
33    -> monad -> 'a1 **)
34let rec monad_rect_Type5 h_mk_Monad x_1736 =
35  let { m_return = m_return0; m_bind = m_bind0 } = x_1736 in
36  h_mk_Monad __ m_return0 m_bind0
37
38(** val monad_rect_Type3 :
39    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
40    -> monad -> 'a1 **)
41let rec monad_rect_Type3 h_mk_Monad x_1738 =
42  let { m_return = m_return0; m_bind = m_bind0 } = x_1738 in
43  h_mk_Monad __ m_return0 m_bind0
44
45(** val monad_rect_Type2 :
46    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
47    -> monad -> 'a1 **)
48let rec monad_rect_Type2 h_mk_Monad x_1740 =
49  let { m_return = m_return0; m_bind = m_bind0 } = x_1740 in
50  h_mk_Monad __ m_return0 m_bind0
51
52(** val monad_rect_Type1 :
53    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
54    -> monad -> 'a1 **)
55let rec monad_rect_Type1 h_mk_Monad x_1742 =
56  let { m_return = m_return0; m_bind = m_bind0 } = x_1742 in
57  h_mk_Monad __ m_return0 m_bind0
58
59(** val monad_rect_Type0 :
60    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
61    -> monad -> 'a1 **)
62let rec monad_rect_Type0 h_mk_Monad x_1744 =
63  let { m_return = m_return0; m_bind = m_bind0 } = x_1744 in
64  h_mk_Monad __ m_return0 m_bind0
65
66type 'x monad0 = __
67
68(** val m_return0 : monad -> 'a1 -> __ **)
69let rec m_return0 xxx x_1761 =
70  (let { m_return = yyy; m_bind = x0 } = xxx in Obj.magic yyy) __ x_1761
71
72(** val m_bind0 : monad -> __ -> ('a1 -> __) -> __ **)
73let rec m_bind0 xxx x_1758 x_1759 =
74  (let { m_return = x0; m_bind = yyy } = xxx in Obj.magic yyy) __ __ x_1758
75    x_1759
76
77(** val monad_inv_rect_Type4 :
78    monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
79    -> __ -> 'a1) -> 'a1 **)
80let monad_inv_rect_Type4 hterm h1 =
81  let hcut = monad_rect_Type4 h1 hterm in hcut __
82
83(** val monad_inv_rect_Type3 :
84    monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
85    -> __ -> 'a1) -> 'a1 **)
86let monad_inv_rect_Type3 hterm h1 =
87  let hcut = monad_rect_Type3 h1 hterm in hcut __
88
89(** val monad_inv_rect_Type2 :
90    monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
91    -> __ -> 'a1) -> 'a1 **)
92let monad_inv_rect_Type2 hterm h1 =
93  let hcut = monad_rect_Type2 h1 hterm in hcut __
94
95(** val monad_inv_rect_Type1 :
96    monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
97    -> __ -> 'a1) -> 'a1 **)
98let monad_inv_rect_Type1 hterm h1 =
99  let hcut = monad_rect_Type1 h1 hterm in hcut __
100
101(** val monad_inv_rect_Type0 :
102    monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
103    -> __ -> 'a1) -> 'a1 **)
104let monad_inv_rect_Type0 hterm h1 =
105  let hcut = monad_rect_Type0 h1 hterm in hcut __
106
107type monadProps =
108  monad
109  (* singleton inductive, whose constructor was mk_MonadProps *)
110
111(** val monadProps_rect_Type4 :
112    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
113let rec monadProps_rect_Type4 h_mk_MonadProps x_1765 =
114  let max_def = x_1765 in h_mk_MonadProps max_def __ __ __ __
115
116(** val monadProps_rect_Type5 :
117    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
118let rec monadProps_rect_Type5 h_mk_MonadProps x_1767 =
119  let max_def = x_1767 in h_mk_MonadProps max_def __ __ __ __
120
121(** val monadProps_rect_Type3 :
122    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
123let rec monadProps_rect_Type3 h_mk_MonadProps x_1769 =
124  let max_def = x_1769 in h_mk_MonadProps max_def __ __ __ __
125
126(** val monadProps_rect_Type2 :
127    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
128let rec monadProps_rect_Type2 h_mk_MonadProps x_1771 =
129  let max_def = x_1771 in h_mk_MonadProps max_def __ __ __ __
130
131(** val monadProps_rect_Type1 :
132    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
133let rec monadProps_rect_Type1 h_mk_MonadProps x_1773 =
134  let max_def = x_1773 in h_mk_MonadProps max_def __ __ __ __
135
136(** val monadProps_rect_Type0 :
137    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
138let rec monadProps_rect_Type0 h_mk_MonadProps x_1775 =
139  let max_def = x_1775 in h_mk_MonadProps max_def __ __ __ __
140
141(** val max_def : monadProps -> monad **)
142let rec max_def xxx =
143  let yyy = xxx in yyy
144
145(** val monadProps_inv_rect_Type4 :
146    monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
147let monadProps_inv_rect_Type4 hterm h1 =
148  let hcut = monadProps_rect_Type4 h1 hterm in hcut __
149
150(** val monadProps_inv_rect_Type3 :
151    monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
152let monadProps_inv_rect_Type3 hterm h1 =
153  let hcut = monadProps_rect_Type3 h1 hterm in hcut __
154
155(** val monadProps_inv_rect_Type2 :
156    monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
157let monadProps_inv_rect_Type2 hterm h1 =
158  let hcut = monadProps_rect_Type2 h1 hterm in hcut __
159
160(** val monadProps_inv_rect_Type1 :
161    monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
162let monadProps_inv_rect_Type1 hterm h1 =
163  let hcut = monadProps_rect_Type1 h1 hterm in hcut __
164
165(** val monadProps_inv_rect_Type0 :
166    monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
167let monadProps_inv_rect_Type0 hterm h1 =
168  let hcut = monadProps_rect_Type0 h1 hterm in hcut __
169
170type 'x_1762 max_def__o__monad = __
171
172type setoidMonadProps =
173  monad
174  (* singleton inductive, whose constructor was mk_SetoidMonadProps *)
175
176(** val setoidMonadProps_rect_Type4 :
177    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
178    setoidMonadProps -> 'a1 **)
179let rec setoidMonadProps_rect_Type4 h_mk_SetoidMonadProps x_1797 =
180  let smax_def = x_1797 in
181  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
182
183(** val setoidMonadProps_rect_Type5 :
184    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
185    setoidMonadProps -> 'a1 **)
186let rec setoidMonadProps_rect_Type5 h_mk_SetoidMonadProps x_1799 =
187  let smax_def = x_1799 in
188  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
189
190(** val setoidMonadProps_rect_Type3 :
191    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
192    setoidMonadProps -> 'a1 **)
193let rec setoidMonadProps_rect_Type3 h_mk_SetoidMonadProps x_1801 =
194  let smax_def = x_1801 in
195  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
196
197(** val setoidMonadProps_rect_Type2 :
198    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
199    setoidMonadProps -> 'a1 **)
200let rec setoidMonadProps_rect_Type2 h_mk_SetoidMonadProps x_1803 =
201  let smax_def = x_1803 in
202  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
203
204(** val setoidMonadProps_rect_Type1 :
205    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
206    setoidMonadProps -> 'a1 **)
207let rec setoidMonadProps_rect_Type1 h_mk_SetoidMonadProps x_1805 =
208  let smax_def = x_1805 in
209  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
210
211(** val setoidMonadProps_rect_Type0 :
212    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
213    setoidMonadProps -> 'a1 **)
214let rec setoidMonadProps_rect_Type0 h_mk_SetoidMonadProps x_1807 =
215  let smax_def = x_1807 in
216  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
217
218(** val smax_def : setoidMonadProps -> monad **)
219let rec smax_def xxx =
220  let yyy = xxx in yyy
221
222type 'x sm_eq = __
223
224(** val setoidMonadProps_inv_rect_Type4 :
225    setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
226    __ -> __ -> __ -> 'a1) -> 'a1 **)
227let setoidMonadProps_inv_rect_Type4 hterm h1 =
228  let hcut = setoidMonadProps_rect_Type4 h1 hterm in hcut __
229
230(** val setoidMonadProps_inv_rect_Type3 :
231    setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
232    __ -> __ -> __ -> 'a1) -> 'a1 **)
233let setoidMonadProps_inv_rect_Type3 hterm h1 =
234  let hcut = setoidMonadProps_rect_Type3 h1 hterm in hcut __
235
236(** val setoidMonadProps_inv_rect_Type2 :
237    setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
238    __ -> __ -> __ -> 'a1) -> 'a1 **)
239let setoidMonadProps_inv_rect_Type2 hterm h1 =
240  let hcut = setoidMonadProps_rect_Type2 h1 hterm in hcut __
241
242(** val setoidMonadProps_inv_rect_Type1 :
243    setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
244    __ -> __ -> __ -> 'a1) -> 'a1 **)
245let setoidMonadProps_inv_rect_Type1 hterm h1 =
246  let hcut = setoidMonadProps_rect_Type1 h1 hterm in hcut __
247
248(** val setoidMonadProps_inv_rect_Type0 :
249    setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
250    __ -> __ -> __ -> 'a1) -> 'a1 **)
251let setoidMonadProps_inv_rect_Type0 hterm h1 =
252  let hcut = setoidMonadProps_rect_Type0 h1 hterm in hcut __
253
254type 'x_1762 smax_def__o__monad = __
255
256(** val setoid_of_monad : setoidMonadProps -> Setoids.setoid **)
257let setoid_of_monad m =
258  Setoids.Mk_Setoid
259
260open Bool
261
262open Nat
263
264open List
265
266(** val m_map : monad -> ('a1 -> 'a2) -> __ -> __ **)
267let m_map m f m0 =
268  m_bind0 m m0 (fun x -> m_return0 m (f x))
269
270(** val m_map2 : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __ **)
271let m_map2 m f m0 n =
272  m_bind0 m m0 (fun x -> m_bind0 m n (fun y -> m_return0 m (f x y)))
273
274(** val m_bind2 : monad -> __ -> ('a1 -> 'a2 -> __) -> __ **)
275let m_bind2 m m0 f =
276  m_bind0 m m0 (fun p -> f p.Types.fst p.Types.snd)
277
278(** val m_bind3 : monad -> __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __ **)
279let m_bind3 m m0 f =
280  m_bind0 m m0 (fun p ->
281    f p.Types.fst.Types.fst p.Types.fst.Types.snd p.Types.snd)
282
283(** val m_join : monad -> __ -> __ **)
284let m_join m m0 =
285  m_bind0 m m0 (fun x -> x)
286
287(** val m_sigbind2 : monad -> __ -> ('a1 -> 'a2 -> __ -> __) -> __ **)
288let m_sigbind2 m e f =
289  m_bind0 m e (fun e_sig ->
290    let p = e_sig in
291    (let { Types.fst = a; Types.snd = b } = p in (fun _ -> f a b __)) __)
292
293(** val m_list_map : monad -> ('a1 -> __) -> 'a1 List.list -> __ **)
294let m_list_map m f l =
295  List.foldr (fun el macc ->
296    m_bind0 m (f el) (fun r ->
297      m_bind0 m macc (fun acc -> m_return0 m (List.Cons (r, acc)))))
298    (m_return0 m List.Nil) l
299
300(** val m_list_map_sigma : monad -> ('a1 -> __) -> 'a1 List.list -> __ **)
301let m_list_map_sigma m f l =
302  List.foldr (fun el macc ->
303    m_bind0 m (f el) (fun eta681 ->
304      let r = eta681 in
305      m_bind0 m macc (fun eta680 ->
306        let acc = eta680 in m_return0 m (List.Cons (r, acc)))))
307    (m_return0 m List.Nil) l
308
309(** val m_bin_op : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __ **)
310let m_bin_op m op0 m0 n =
311  m_bind0 m m0 (fun x -> m_bind0 m n (fun y -> m_return0 m (op0 x y)))
312
313(** val m_fold :
314    monad -> ('a1 -> 'a2 -> __) -> 'a1 List.list -> 'a2 -> __ **)
315let rec m_fold m f l init =
316  match l with
317  | List.Nil -> m_return0 m init
318  | List.Cons (hd0, tl) -> m_bind0 m (f hd0 init) (fun y -> m_fold m f tl y)
319
320(** val makeMonadProps :
321    (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) ->
322    monadProps **)
323let makeMonadProps m_return1 m_bind1 =
324  { m_return = (Obj.magic m_return1); m_bind = (Obj.magic m_bind1) }
325
326(** val makeSetoidMonadProps :
327    (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) ->
328    setoidMonadProps **)
329let makeSetoidMonadProps m_return1 m_bind1 =
330  { m_return = (Obj.magic m_return1); m_bind = (Obj.magic m_bind1) }
331
332open Jmeq
333
334open Russell
335
336type monadPred =
337| Mk_MonadPred
338
339(** val monadPred_rect_Type4 :
340    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
341let rec monadPred_rect_Type4 m h_mk_MonadPred = function
342| Mk_MonadPred -> h_mk_MonadPred __ __ __ __
343
344(** val monadPred_rect_Type5 :
345    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
346let rec monadPred_rect_Type5 m h_mk_MonadPred = function
347| Mk_MonadPred -> h_mk_MonadPred __ __ __ __
348
349(** val monadPred_rect_Type3 :
350    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
351let rec monadPred_rect_Type3 m h_mk_MonadPred = function
352| Mk_MonadPred -> h_mk_MonadPred __ __ __ __
353
354(** val monadPred_rect_Type2 :
355    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
356let rec monadPred_rect_Type2 m h_mk_MonadPred = function
357| Mk_MonadPred -> h_mk_MonadPred __ __ __ __
358
359(** val monadPred_rect_Type1 :
360    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
361let rec monadPred_rect_Type1 m h_mk_MonadPred = function
362| Mk_MonadPred -> h_mk_MonadPred __ __ __ __
363
364(** val monadPred_rect_Type0 :
365    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
366let rec monadPred_rect_Type0 m h_mk_MonadPred = function
367| Mk_MonadPred -> h_mk_MonadPred __ __ __ __
368
369type 'x m_pred = __
370
371(** val monadPred_inv_rect_Type4 :
372    monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
373let monadPred_inv_rect_Type4 x1 hterm h1 =
374  let hcut = monadPred_rect_Type4 x1 h1 hterm in hcut __
375
376(** val monadPred_inv_rect_Type3 :
377    monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
378let monadPred_inv_rect_Type3 x1 hterm h1 =
379  let hcut = monadPred_rect_Type3 x1 h1 hterm in hcut __
380
381(** val monadPred_inv_rect_Type2 :
382    monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
383let monadPred_inv_rect_Type2 x1 hterm h1 =
384  let hcut = monadPred_rect_Type2 x1 h1 hterm in hcut __
385
386(** val monadPred_inv_rect_Type1 :
387    monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
388let monadPred_inv_rect_Type1 x1 hterm h1 =
389  let hcut = monadPred_rect_Type1 x1 h1 hterm in hcut __
390
391(** val monadPred_inv_rect_Type0 :
392    monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
393let monadPred_inv_rect_Type0 x1 hterm h1 =
394  let hcut = monadPred_rect_Type0 x1 h1 hterm in hcut __
395
396(** val monadPred_jmdiscr : monad -> monadPred -> monadPred -> __ **)
397let monadPred_jmdiscr a1 x y =
398  Logic.eq_rect_Type2 x
399    (let Mk_MonadPred = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
400
401type injMonadPred = { im_pred : monadPred;
402                      mp_inject : (__ -> __ -> __ Types.sig0 -> __) }
403
404(** val injMonadPred_rect_Type4 :
405    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
406    injMonadPred -> 'a1 **)
407let rec injMonadPred_rect_Type4 m h_mk_InjMonadPred x_1867 =
408  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1867 in
409  h_mk_InjMonadPred im_pred0 mp_inject0 __
410
411(** val injMonadPred_rect_Type5 :
412    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
413    injMonadPred -> 'a1 **)
414let rec injMonadPred_rect_Type5 m h_mk_InjMonadPred x_1869 =
415  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1869 in
416  h_mk_InjMonadPred im_pred0 mp_inject0 __
417
418(** val injMonadPred_rect_Type3 :
419    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
420    injMonadPred -> 'a1 **)
421let rec injMonadPred_rect_Type3 m h_mk_InjMonadPred x_1871 =
422  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1871 in
423  h_mk_InjMonadPred im_pred0 mp_inject0 __
424
425(** val injMonadPred_rect_Type2 :
426    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
427    injMonadPred -> 'a1 **)
428let rec injMonadPred_rect_Type2 m h_mk_InjMonadPred x_1873 =
429  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1873 in
430  h_mk_InjMonadPred im_pred0 mp_inject0 __
431
432(** val injMonadPred_rect_Type1 :
433    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
434    injMonadPred -> 'a1 **)
435let rec injMonadPred_rect_Type1 m h_mk_InjMonadPred x_1875 =
436  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1875 in
437  h_mk_InjMonadPred im_pred0 mp_inject0 __
438
439(** val injMonadPred_rect_Type0 :
440    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
441    injMonadPred -> 'a1 **)
442let rec injMonadPred_rect_Type0 m h_mk_InjMonadPred x_1877 =
443  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1877 in
444  h_mk_InjMonadPred im_pred0 mp_inject0 __
445
446(** val im_pred : monad -> injMonadPred -> monadPred **)
447let rec im_pred m xxx =
448  xxx.im_pred
449
450(** val mp_inject0 : monad -> injMonadPred -> __ Types.sig0 -> __ **)
451let rec mp_inject0 m xxx x_1892 =
452  (xxx.mp_inject) __ __ x_1892
453
454(** val injMonadPred_inv_rect_Type4 :
455    monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
456    -> __ -> __ -> 'a1) -> 'a1 **)
457let injMonadPred_inv_rect_Type4 x1 hterm h1 =
458  let hcut = injMonadPred_rect_Type4 x1 h1 hterm in hcut __
459
460(** val injMonadPred_inv_rect_Type3 :
461    monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
462    -> __ -> __ -> 'a1) -> 'a1 **)
463let injMonadPred_inv_rect_Type3 x1 hterm h1 =
464  let hcut = injMonadPred_rect_Type3 x1 h1 hterm in hcut __
465
466(** val injMonadPred_inv_rect_Type2 :
467    monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
468    -> __ -> __ -> 'a1) -> 'a1 **)
469let injMonadPred_inv_rect_Type2 x1 hterm h1 =
470  let hcut = injMonadPred_rect_Type2 x1 h1 hterm in hcut __
471
472(** val injMonadPred_inv_rect_Type1 :
473    monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
474    -> __ -> __ -> 'a1) -> 'a1 **)
475let injMonadPred_inv_rect_Type1 x1 hterm h1 =
476  let hcut = injMonadPred_rect_Type1 x1 h1 hterm in hcut __
477
478(** val injMonadPred_inv_rect_Type0 :
479    monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
480    -> __ -> __ -> 'a1) -> 'a1 **)
481let injMonadPred_inv_rect_Type0 x1 hterm h1 =
482  let hcut = injMonadPred_rect_Type0 x1 h1 hterm in hcut __
483
484(** val injMonadPred_jmdiscr :
485    monad -> injMonadPred -> injMonadPred -> __ **)
486let injMonadPred_jmdiscr a1 x y =
487  Logic.eq_rect_Type2 x
488    (let { im_pred = a0; mp_inject = a10 } = x in
489    Obj.magic (fun _ dH -> dH __ __ __)) y
490
491type monadRel =
492| Mk_MonadRel
493
494(** val monadRel_rect_Type4 :
495    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
496let rec monadRel_rect_Type4 m1 m2 h_mk_MonadRel = function
497| Mk_MonadRel -> h_mk_MonadRel __ __ __ __
498
499(** val monadRel_rect_Type5 :
500    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
501let rec monadRel_rect_Type5 m1 m2 h_mk_MonadRel = function
502| Mk_MonadRel -> h_mk_MonadRel __ __ __ __
503
504(** val monadRel_rect_Type3 :
505    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
506let rec monadRel_rect_Type3 m1 m2 h_mk_MonadRel = function
507| Mk_MonadRel -> h_mk_MonadRel __ __ __ __
508
509(** val monadRel_rect_Type2 :
510    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
511let rec monadRel_rect_Type2 m1 m2 h_mk_MonadRel = function
512| Mk_MonadRel -> h_mk_MonadRel __ __ __ __
513
514(** val monadRel_rect_Type1 :
515    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
516let rec monadRel_rect_Type1 m1 m2 h_mk_MonadRel = function
517| Mk_MonadRel -> h_mk_MonadRel __ __ __ __
518
519(** val monadRel_rect_Type0 :
520    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
521let rec monadRel_rect_Type0 m1 m2 h_mk_MonadRel = function
522| Mk_MonadRel -> h_mk_MonadRel __ __ __ __
523
524type ('x, 'x0) m_rel = __
525
526(** val monadRel_inv_rect_Type4 :
527    monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
528let monadRel_inv_rect_Type4 x1 x2 hterm h1 =
529  let hcut = monadRel_rect_Type4 x1 x2 h1 hterm in hcut __
530
531(** val monadRel_inv_rect_Type3 :
532    monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
533let monadRel_inv_rect_Type3 x1 x2 hterm h1 =
534  let hcut = monadRel_rect_Type3 x1 x2 h1 hterm in hcut __
535
536(** val monadRel_inv_rect_Type2 :
537    monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
538let monadRel_inv_rect_Type2 x1 x2 hterm h1 =
539  let hcut = monadRel_rect_Type2 x1 x2 h1 hterm in hcut __
540
541(** val monadRel_inv_rect_Type1 :
542    monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
543let monadRel_inv_rect_Type1 x1 x2 hterm h1 =
544  let hcut = monadRel_rect_Type1 x1 x2 h1 hterm in hcut __
545
546(** val monadRel_inv_rect_Type0 :
547    monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
548let monadRel_inv_rect_Type0 x1 x2 hterm h1 =
549  let hcut = monadRel_rect_Type0 x1 x2 h1 hterm in hcut __
550
551(** val monadRel_jmdiscr : monad -> monad -> monadRel -> monadRel -> __ **)
552let monadRel_jmdiscr a1 a2 x y =
553  Logic.eq_rect_Type2 x
554    (let Mk_MonadRel = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
555
Note: See TracBrowser for help on using the repository browser.