source: extracted/monad.ml @ 2729

Last change on this file since 2729 was 2649, checked in by sacerdot, 7 years ago

...

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 'a 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 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 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 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.