17 type ('a, 'b) pred_transformer = __
19 type ('a, 'b, 'c, 'd) rel_transformer = __
21 type monad = { m_return : (__ -> __ -> __);
22 m_bind : (__ -> __ -> __ -> (__ -> __) -> __) }
24 (** val monad_rect_Type4 :
25 (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
27 let rec monad_rect_Type4 h_mk_Monad x_744 =
28 let { m_return = m_return0; m_bind = m_bind0 } = x_744 in
29 h_mk_Monad __ m_return0 m_bind0
31 (** val monad_rect_Type5 :
32 (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
34 let rec monad_rect_Type5 h_mk_Monad x_746 =
35 let { m_return = m_return0; m_bind = m_bind0 } = x_746 in
36 h_mk_Monad __ m_return0 m_bind0
38 (** val monad_rect_Type3 :
39 (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
41 let rec monad_rect_Type3 h_mk_Monad x_748 =
42 let { m_return = m_return0; m_bind = m_bind0 } = x_748 in
43 h_mk_Monad __ m_return0 m_bind0
45 (** val monad_rect_Type2 :
46 (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
48 let rec monad_rect_Type2 h_mk_Monad x_750 =
49 let { m_return = m_return0; m_bind = m_bind0 } = x_750 in
50 h_mk_Monad __ m_return0 m_bind0
52 (** val monad_rect_Type1 :
53 (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
55 let rec monad_rect_Type1 h_mk_Monad x_752 =
56 let { m_return = m_return0; m_bind = m_bind0 } = x_752 in
57 h_mk_Monad __ m_return0 m_bind0
59 (** val monad_rect_Type0 :
60 (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
62 let rec monad_rect_Type0 h_mk_Monad x_754 =
63 let { m_return = m_return0; m_bind = m_bind0 } = x_754 in
64 h_mk_Monad __ m_return0 m_bind0
68 (** val m_return0 : monad -> 'a1 -> __ **)
69 let rec m_return0 xxx x_771 =
70 (let { m_return = yyy; m_bind = x0 } = xxx in Obj.magic yyy) __ x_771
72 (** val m_bind0 : monad -> __ -> ('a1 -> __) -> __ **)
73 let rec m_bind0 xxx x_768 x_769 =
74 (let { m_return = x0; m_bind = yyy } = xxx in Obj.magic yyy) __ __ x_768
77 (** val monad_inv_rect_Type4 :
78 monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
79 -> __ -> 'a1) -> 'a1 **)
80 let monad_inv_rect_Type4 hterm h1 =
81 let hcut = monad_rect_Type4 h1 hterm in hcut __
83 (** val monad_inv_rect_Type3 :
84 monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
85 -> __ -> 'a1) -> 'a1 **)
86 let monad_inv_rect_Type3 hterm h1 =
87 let hcut = monad_rect_Type3 h1 hterm in hcut __
89 (** val monad_inv_rect_Type2 :
90 monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
91 -> __ -> 'a1) -> 'a1 **)
92 let monad_inv_rect_Type2 hterm h1 =
93 let hcut = monad_rect_Type2 h1 hterm in hcut __
95 (** val monad_inv_rect_Type1 :
96 monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
97 -> __ -> 'a1) -> 'a1 **)
98 let monad_inv_rect_Type1 hterm h1 =
99 let hcut = monad_rect_Type1 h1 hterm in hcut __
101 (** val monad_inv_rect_Type0 :
102 monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
103 -> __ -> 'a1) -> 'a1 **)
104 let monad_inv_rect_Type0 hterm h1 =
105 let hcut = monad_rect_Type0 h1 hterm in hcut __
109 (* singleton inductive, whose constructor was mk_MonadProps *)
111 (** val monadProps_rect_Type4 :
112 (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
113 let rec monadProps_rect_Type4 h_mk_MonadProps x_775 =
114 let max_def = x_775 in h_mk_MonadProps max_def __ __ __ __
116 (** val monadProps_rect_Type5 :
117 (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
118 let rec monadProps_rect_Type5 h_mk_MonadProps x_777 =
119 let max_def = x_777 in h_mk_MonadProps max_def __ __ __ __
121 (** val monadProps_rect_Type3 :
122 (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
123 let rec monadProps_rect_Type3 h_mk_MonadProps x_779 =
124 let max_def = x_779 in h_mk_MonadProps max_def __ __ __ __
126 (** val monadProps_rect_Type2 :
127 (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
128 let rec monadProps_rect_Type2 h_mk_MonadProps x_781 =
129 let max_def = x_781 in h_mk_MonadProps max_def __ __ __ __
131 (** val monadProps_rect_Type1 :
132 (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
133 let rec monadProps_rect_Type1 h_mk_MonadProps x_783 =
134 let max_def = x_783 in h_mk_MonadProps max_def __ __ __ __
136 (** val monadProps_rect_Type0 :
137 (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
138 let rec monadProps_rect_Type0 h_mk_MonadProps x_785 =
139 let max_def = x_785 in h_mk_MonadProps max_def __ __ __ __
141 (** val max_def : monadProps -> monad **)
142 let rec max_def xxx =
145 (** val monadProps_inv_rect_Type4 :
146 monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
147 let monadProps_inv_rect_Type4 hterm h1 =
148 let hcut = monadProps_rect_Type4 h1 hterm in hcut __
150 (** val monadProps_inv_rect_Type3 :
151 monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
152 let monadProps_inv_rect_Type3 hterm h1 =
153 let hcut = monadProps_rect_Type3 h1 hterm in hcut __
155 (** val monadProps_inv_rect_Type2 :
156 monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
157 let monadProps_inv_rect_Type2 hterm h1 =
158 let hcut = monadProps_rect_Type2 h1 hterm in hcut __
160 (** val monadProps_inv_rect_Type1 :
161 monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
162 let monadProps_inv_rect_Type1 hterm h1 =
163 let hcut = monadProps_rect_Type1 h1 hterm in hcut __
165 (** val monadProps_inv_rect_Type0 :
166 monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
167 let monadProps_inv_rect_Type0 hterm h1 =
168 let hcut = monadProps_rect_Type0 h1 hterm in hcut __
170 type 'x_772 max_def__o__monad = __
172 type setoidMonadProps =
174 (* singleton inductive, whose constructor was mk_SetoidMonadProps *)
176 (** val setoidMonadProps_rect_Type4 :
177 (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
178 setoidMonadProps -> 'a1 **)
179 let rec setoidMonadProps_rect_Type4 h_mk_SetoidMonadProps x_807 =
180 let smax_def = x_807 in
181 h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
183 (** val setoidMonadProps_rect_Type5 :
184 (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
185 setoidMonadProps -> 'a1 **)
186 let rec setoidMonadProps_rect_Type5 h_mk_SetoidMonadProps x_809 =
187 let smax_def = x_809 in
188 h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
190 (** val setoidMonadProps_rect_Type3 :
191 (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
192 setoidMonadProps -> 'a1 **)
193 let rec setoidMonadProps_rect_Type3 h_mk_SetoidMonadProps x_811 =
194 let smax_def = x_811 in
195 h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
197 (** val setoidMonadProps_rect_Type2 :
198 (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
199 setoidMonadProps -> 'a1 **)
200 let rec setoidMonadProps_rect_Type2 h_mk_SetoidMonadProps x_813 =
201 let smax_def = x_813 in
202 h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
204 (** val setoidMonadProps_rect_Type1 :
205 (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
206 setoidMonadProps -> 'a1 **)
207 let rec setoidMonadProps_rect_Type1 h_mk_SetoidMonadProps x_815 =
208 let smax_def = x_815 in
209 h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
211 (** val setoidMonadProps_rect_Type0 :
212 (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
213 setoidMonadProps -> 'a1 **)
214 let rec setoidMonadProps_rect_Type0 h_mk_SetoidMonadProps x_817 =
215 let smax_def = x_817 in
216 h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
218 (** val smax_def : setoidMonadProps -> monad **)
219 let rec smax_def xxx =
222 (** val setoidMonadProps_inv_rect_Type4 :
223 setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
224 __ -> __ -> __ -> 'a1) -> 'a1 **)
225 let setoidMonadProps_inv_rect_Type4 hterm h1 =
226 let hcut = setoidMonadProps_rect_Type4 h1 hterm in hcut __
228 (** val setoidMonadProps_inv_rect_Type3 :
229 setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
230 __ -> __ -> __ -> 'a1) -> 'a1 **)
231 let setoidMonadProps_inv_rect_Type3 hterm h1 =
232 let hcut = setoidMonadProps_rect_Type3 h1 hterm in hcut __
234 (** val setoidMonadProps_inv_rect_Type2 :
235 setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
236 __ -> __ -> __ -> 'a1) -> 'a1 **)
237 let setoidMonadProps_inv_rect_Type2 hterm h1 =
238 let hcut = setoidMonadProps_rect_Type2 h1 hterm in hcut __
240 (** val setoidMonadProps_inv_rect_Type1 :
241 setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
242 __ -> __ -> __ -> 'a1) -> 'a1 **)
243 let setoidMonadProps_inv_rect_Type1 hterm h1 =
244 let hcut = setoidMonadProps_rect_Type1 h1 hterm in hcut __
246 (** val setoidMonadProps_inv_rect_Type0 :
247 setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
248 __ -> __ -> __ -> 'a1) -> 'a1 **)
249 let setoidMonadProps_inv_rect_Type0 hterm h1 =
250 let hcut = setoidMonadProps_rect_Type0 h1 hterm in hcut __
252 type 'x_772 smax_def__o__monad = __
254 (** val setoid_of_monad : setoidMonadProps -> Setoids.setoid **)
255 let setoid_of_monad m =
264 (** val m_map : monad -> ('a1 -> 'a2) -> __ -> __ **)
266 m_bind0 m m0 (fun x -> m_return0 m (f x))
268 (** val m_map2 : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __ **)
269 let m_map2 m f m0 n =
270 m_bind0 m m0 (fun x -> m_bind0 m n (fun y -> m_return0 m (f x y)))
272 (** val m_bind2 : monad -> __ -> ('a1 -> 'a2 -> __) -> __ **)
274 m_bind0 m m0 (fun p -> f p.Types.fst p.Types.snd)
276 (** val m_bind3 : monad -> __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __ **)
278 m_bind0 m m0 (fun p ->
279 f p.Types.fst.Types.fst p.Types.fst.Types.snd p.Types.snd)
281 (** val m_join : monad -> __ -> __ **)
283 m_bind0 m m0 (fun x -> x)
285 (** val m_sigbind2 : monad -> __ -> ('a1 -> 'a2 -> __ -> __) -> __ **)
286 let m_sigbind2 m e f =
287 m_bind0 m e (fun e_sig ->
289 (let { Types.fst = a; Types.snd = b } = p in (fun _ -> f a b __)) __)
291 (** val m_list_map : monad -> ('a1 -> __) -> 'a1 List.list -> __ **)
292 let m_list_map m f l =
293 List.foldr (fun el macc ->
294 m_bind0 m (f el) (fun r ->
295 m_bind0 m macc (fun acc -> m_return0 m (List.Cons (r, acc)))))
296 (m_return0 m List.Nil) l
298 (** val m_list_map_sigma : monad -> ('a1 -> __) -> 'a1 List.list -> __ **)
299 let m_list_map_sigma m f l =
300 List.foldr (fun el macc ->
301 m_bind0 m (f el) (fun eta285 ->
303 m_bind0 m macc (fun eta284 ->
304 let acc = eta284 in m_return0 m (List.Cons (r, acc)))))
305 (m_return0 m List.Nil) l
307 (** val m_bin_op : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __ **)
308 let m_bin_op m op m0 n =
309 m_bind0 m m0 (fun x -> m_bind0 m n (fun y -> m_return0 m (op x y)))
312 monad -> ('a1 -> 'a2 -> __) -> 'a1 List.list -> 'a2 -> __ **)
313 let rec m_fold m f l init =
315 | List.Nil -> m_return0 m init
316 | List.Cons (hd, tl) -> m_bind0 m (f hd init) (fun y -> m_fold m f tl y)
318 (** val makeMonadProps :
319 (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) ->
321 let makeMonadProps m_return1 m_bind1 =
322 { m_return = (Obj.magic m_return1); m_bind = (Obj.magic m_bind1) }
324 (** val makeSetoidMonadProps :
325 (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) ->
327 let makeSetoidMonadProps m_return1 m_bind1 =
328 { m_return = (Obj.magic m_return1); m_bind = (Obj.magic m_bind1) }
337 (** val monadPred_rect_Type4 :
338 monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
339 let rec monadPred_rect_Type4 m h_mk_MonadPred = function
340 | Mk_MonadPred -> h_mk_MonadPred __ __ __ __
342 (** val monadPred_rect_Type5 :
343 monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
344 let rec monadPred_rect_Type5 m h_mk_MonadPred = function
345 | Mk_MonadPred -> h_mk_MonadPred __ __ __ __
347 (** val monadPred_rect_Type3 :
348 monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
349 let rec monadPred_rect_Type3 m h_mk_MonadPred = function
350 | Mk_MonadPred -> h_mk_MonadPred __ __ __ __
352 (** val monadPred_rect_Type2 :
353 monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
354 let rec monadPred_rect_Type2 m h_mk_MonadPred = function
355 | Mk_MonadPred -> h_mk_MonadPred __ __ __ __
357 (** val monadPred_rect_Type1 :
358 monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
359 let rec monadPred_rect_Type1 m h_mk_MonadPred = function
360 | Mk_MonadPred -> h_mk_MonadPred __ __ __ __
362 (** val monadPred_rect_Type0 :
363 monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
364 let rec monadPred_rect_Type0 m h_mk_MonadPred = function
365 | Mk_MonadPred -> h_mk_MonadPred __ __ __ __
367 (** val monadPred_inv_rect_Type4 :
368 monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
369 let monadPred_inv_rect_Type4 x1 hterm h1 =
370 let hcut = monadPred_rect_Type4 x1 h1 hterm in hcut __
372 (** val monadPred_inv_rect_Type3 :
373 monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
374 let monadPred_inv_rect_Type3 x1 hterm h1 =
375 let hcut = monadPred_rect_Type3 x1 h1 hterm in hcut __
377 (** val monadPred_inv_rect_Type2 :
378 monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
379 let monadPred_inv_rect_Type2 x1 hterm h1 =
380 let hcut = monadPred_rect_Type2 x1 h1 hterm in hcut __
382 (** val monadPred_inv_rect_Type1 :
383 monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
384 let monadPred_inv_rect_Type1 x1 hterm h1 =
385 let hcut = monadPred_rect_Type1 x1 h1 hterm in hcut __
387 (** val monadPred_inv_rect_Type0 :
388 monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
389 let monadPred_inv_rect_Type0 x1 hterm h1 =
390 let hcut = monadPred_rect_Type0 x1 h1 hterm in hcut __
392 (** val monadPred_jmdiscr : monad -> monadPred -> monadPred -> __ **)
393 let monadPred_jmdiscr a1 x y =
394 Logic.eq_rect_Type2 x
395 (let Mk_MonadPred = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
397 type injMonadPred = { im_pred : monadPred;
398 mp_inject : (__ -> __ -> __ Types.sig0 -> __) }
400 (** val injMonadPred_rect_Type4 :
401 monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
402 injMonadPred -> 'a1 **)
403 let rec injMonadPred_rect_Type4 m h_mk_InjMonadPred x_1048 =
404 let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1048 in
405 h_mk_InjMonadPred im_pred0 mp_inject0 __
407 (** val injMonadPred_rect_Type5 :
408 monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
409 injMonadPred -> 'a1 **)
410 let rec injMonadPred_rect_Type5 m h_mk_InjMonadPred x_1050 =
411 let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1050 in
412 h_mk_InjMonadPred im_pred0 mp_inject0 __
414 (** val injMonadPred_rect_Type3 :
415 monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
416 injMonadPred -> 'a1 **)
417 let rec injMonadPred_rect_Type3 m h_mk_InjMonadPred x_1052 =
418 let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1052 in
419 h_mk_InjMonadPred im_pred0 mp_inject0 __
421 (** val injMonadPred_rect_Type2 :
422 monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
423 injMonadPred -> 'a1 **)
424 let rec injMonadPred_rect_Type2 m h_mk_InjMonadPred x_1054 =
425 let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1054 in
426 h_mk_InjMonadPred im_pred0 mp_inject0 __
428 (** val injMonadPred_rect_Type1 :
429 monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
430 injMonadPred -> 'a1 **)
431 let rec injMonadPred_rect_Type1 m h_mk_InjMonadPred x_1056 =
432 let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1056 in
433 h_mk_InjMonadPred im_pred0 mp_inject0 __
435 (** val injMonadPred_rect_Type0 :
436 monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
437 injMonadPred -> 'a1 **)
438 let rec injMonadPred_rect_Type0 m h_mk_InjMonadPred x_1058 =
439 let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1058 in
440 h_mk_InjMonadPred im_pred0 mp_inject0 __
442 (** val im_pred : monad -> injMonadPred -> monadPred **)
443 let rec im_pred m xxx =
446 (** val mp_inject0 : monad -> injMonadPred -> __ Types.sig0 -> __ **)
447 let rec mp_inject0 m xxx x_1073 =
448 (xxx.mp_inject) __ __ x_1073
450 (** val injMonadPred_inv_rect_Type4 :
451 monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
452 -> __ -> __ -> 'a1) -> 'a1 **)
453 let injMonadPred_inv_rect_Type4 x1 hterm h1 =
454 let hcut = injMonadPred_rect_Type4 x1 h1 hterm in hcut __
456 (** val injMonadPred_inv_rect_Type3 :
457 monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
458 -> __ -> __ -> 'a1) -> 'a1 **)
459 let injMonadPred_inv_rect_Type3 x1 hterm h1 =
460 let hcut = injMonadPred_rect_Type3 x1 h1 hterm in hcut __
462 (** val injMonadPred_inv_rect_Type2 :
463 monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
464 -> __ -> __ -> 'a1) -> 'a1 **)
465 let injMonadPred_inv_rect_Type2 x1 hterm h1 =
466 let hcut = injMonadPred_rect_Type2 x1 h1 hterm in hcut __
468 (** val injMonadPred_inv_rect_Type1 :
469 monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
470 -> __ -> __ -> 'a1) -> 'a1 **)
471 let injMonadPred_inv_rect_Type1 x1 hterm h1 =
472 let hcut = injMonadPred_rect_Type1 x1 h1 hterm in hcut __
474 (** val injMonadPred_inv_rect_Type0 :
475 monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
476 -> __ -> __ -> 'a1) -> 'a1 **)
477 let injMonadPred_inv_rect_Type0 x1 hterm h1 =
478 let hcut = injMonadPred_rect_Type0 x1 h1 hterm in hcut __
480 (** val injMonadPred_jmdiscr :
481 monad -> injMonadPred -> injMonadPred -> __ **)
482 let injMonadPred_jmdiscr a1 x y =
483 Logic.eq_rect_Type2 x
484 (let { im_pred = a0; mp_inject = a10 } = x in
485 Obj.magic (fun _ dH -> dH __ __ __)) y
490 (** val monadRel_rect_Type4 :
491 monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
492 let rec monadRel_rect_Type4 m1 m2 h_mk_MonadRel = function
493 | Mk_MonadRel -> h_mk_MonadRel __ __ __ __
495 (** val monadRel_rect_Type5 :
496 monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
497 let rec monadRel_rect_Type5 m1 m2 h_mk_MonadRel = function
498 | Mk_MonadRel -> h_mk_MonadRel __ __ __ __
500 (** val monadRel_rect_Type3 :
501 monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
502 let rec monadRel_rect_Type3 m1 m2 h_mk_MonadRel = function
503 | Mk_MonadRel -> h_mk_MonadRel __ __ __ __
505 (** val monadRel_rect_Type2 :
506 monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
507 let rec monadRel_rect_Type2 m1 m2 h_mk_MonadRel = function
508 | Mk_MonadRel -> h_mk_MonadRel __ __ __ __
510 (** val monadRel_rect_Type1 :
511 monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
512 let rec monadRel_rect_Type1 m1 m2 h_mk_MonadRel = function
513 | Mk_MonadRel -> h_mk_MonadRel __ __ __ __
515 (** val monadRel_rect_Type0 :
516 monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
517 let rec monadRel_rect_Type0 m1 m2 h_mk_MonadRel = function
518 | Mk_MonadRel -> h_mk_MonadRel __ __ __ __
520 (** val monadRel_inv_rect_Type4 :
521 monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
522 let monadRel_inv_rect_Type4 x1 x2 hterm h1 =
523 let hcut = monadRel_rect_Type4 x1 x2 h1 hterm in hcut __
525 (** val monadRel_inv_rect_Type3 :
526 monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
527 let monadRel_inv_rect_Type3 x1 x2 hterm h1 =
528 let hcut = monadRel_rect_Type3 x1 x2 h1 hterm in hcut __
530 (** val monadRel_inv_rect_Type2 :
531 monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
532 let monadRel_inv_rect_Type2 x1 x2 hterm h1 =
533 let hcut = monadRel_rect_Type2 x1 x2 h1 hterm in hcut __
535 (** val monadRel_inv_rect_Type1 :
536 monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
537 let monadRel_inv_rect_Type1 x1 x2 hterm h1 =
538 let hcut = monadRel_rect_Type1 x1 x2 h1 hterm in hcut __
540 (** val monadRel_inv_rect_Type0 :
541 monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
542 let monadRel_inv_rect_Type0 x1 x2 hterm h1 =
543 let hcut = monadRel_rect_Type0 x1 x2 h1 hterm in hcut __
545 (** val monadRel_jmdiscr : monad -> monad -> monadRel -> monadRel -> __ **)
546 let monadRel_jmdiscr a1 a2 x y =
547 Logic.eq_rect_Type2 x
548 (let Mk_MonadRel = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y