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) ->
28 val monad_rect_Type5 :
29 (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
32 val monad_rect_Type3 :
33 (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
36 val monad_rect_Type2 :
37 (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
40 val monad_rect_Type1 :
41 (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
44 val monad_rect_Type0 :
45 (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
50 val m_return0 : monad -> 'a1 -> __
52 val m_bind0 : monad -> __ -> ('a1 -> __) -> __
54 val monad_inv_rect_Type4 :
55 monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
58 val monad_inv_rect_Type3 :
59 monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
62 val monad_inv_rect_Type2 :
63 monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
66 val monad_inv_rect_Type1 :
67 monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
70 val monad_inv_rect_Type0 :
71 monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
76 (* singleton inductive, whose constructor was mk_MonadProps *)
78 val monadProps_rect_Type4 :
79 (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
81 val monadProps_rect_Type5 :
82 (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
84 val monadProps_rect_Type3 :
85 (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
87 val monadProps_rect_Type2 :
88 (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
90 val monadProps_rect_Type1 :
91 (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
93 val monadProps_rect_Type0 :
94 (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
96 val max_def : monadProps -> monad
98 val monadProps_inv_rect_Type4 :
99 monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
101 val monadProps_inv_rect_Type3 :
102 monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
104 val monadProps_inv_rect_Type2 :
105 monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
107 val monadProps_inv_rect_Type1 :
108 monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
110 val monadProps_inv_rect_Type0 :
111 monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
113 type 'x_772 max_def__o__monad = __
115 type setoidMonadProps =
117 (* singleton inductive, whose constructor was mk_SetoidMonadProps *)
119 val setoidMonadProps_rect_Type4 :
120 (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
121 setoidMonadProps -> 'a1
123 val setoidMonadProps_rect_Type5 :
124 (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
125 setoidMonadProps -> 'a1
127 val setoidMonadProps_rect_Type3 :
128 (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
129 setoidMonadProps -> 'a1
131 val setoidMonadProps_rect_Type2 :
132 (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
133 setoidMonadProps -> 'a1
135 val setoidMonadProps_rect_Type1 :
136 (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
137 setoidMonadProps -> 'a1
139 val setoidMonadProps_rect_Type0 :
140 (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
141 setoidMonadProps -> 'a1
143 val smax_def : setoidMonadProps -> monad
145 val setoidMonadProps_inv_rect_Type4 :
146 setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
147 -> __ -> __ -> 'a1) -> 'a1
149 val setoidMonadProps_inv_rect_Type3 :
150 setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
151 -> __ -> __ -> 'a1) -> 'a1
153 val setoidMonadProps_inv_rect_Type2 :
154 setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
155 -> __ -> __ -> 'a1) -> 'a1
157 val setoidMonadProps_inv_rect_Type1 :
158 setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
159 -> __ -> __ -> 'a1) -> 'a1
161 val setoidMonadProps_inv_rect_Type0 :
162 setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
163 -> __ -> __ -> 'a1) -> 'a1
165 type 'x_772 smax_def__o__monad = __
167 val setoid_of_monad : setoidMonadProps -> Setoids.setoid
175 val m_map : monad -> ('a1 -> 'a2) -> __ -> __
177 val m_map2 : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __
179 val m_bind2 : monad -> __ -> ('a1 -> 'a2 -> __) -> __
181 val m_bind3 : monad -> __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __
183 val m_join : monad -> __ -> __
185 val m_sigbind2 : monad -> __ -> ('a1 -> 'a2 -> __ -> __) -> __
187 val m_list_map : monad -> ('a1 -> __) -> 'a1 List.list -> __
189 val m_list_map_sigma : monad -> ('a1 -> __) -> 'a1 List.list -> __
191 val m_bin_op : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __
193 val m_fold : monad -> ('a1 -> 'a2 -> __) -> 'a1 List.list -> 'a2 -> __
196 (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) -> monadProps
198 val makeSetoidMonadProps :
199 (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) ->
209 val monadPred_rect_Type4 :
210 monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
212 val monadPred_rect_Type5 :
213 monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
215 val monadPred_rect_Type3 :
216 monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
218 val monadPred_rect_Type2 :
219 monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
221 val monadPred_rect_Type1 :
222 monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
224 val monadPred_rect_Type0 :
225 monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
227 val monadPred_inv_rect_Type4 :
228 monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
230 val monadPred_inv_rect_Type3 :
231 monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
233 val monadPred_inv_rect_Type2 :
234 monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
236 val monadPred_inv_rect_Type1 :
237 monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
239 val monadPred_inv_rect_Type0 :
240 monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
242 val monadPred_jmdiscr : monad -> monadPred -> monadPred -> __
244 type injMonadPred = { im_pred : monadPred;
245 mp_inject : (__ -> __ -> __ Types.sig0 -> __) }
247 val injMonadPred_rect_Type4 :
248 monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
251 val injMonadPred_rect_Type5 :
252 monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
255 val injMonadPred_rect_Type3 :
256 monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
259 val injMonadPred_rect_Type2 :
260 monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
263 val injMonadPred_rect_Type1 :
264 monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
267 val injMonadPred_rect_Type0 :
268 monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
271 val im_pred : monad -> injMonadPred -> monadPred
273 val mp_inject0 : monad -> injMonadPred -> __ Types.sig0 -> __
275 val injMonadPred_inv_rect_Type4 :
276 monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
277 __ -> __ -> 'a1) -> 'a1
279 val injMonadPred_inv_rect_Type3 :
280 monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
281 __ -> __ -> 'a1) -> 'a1
283 val injMonadPred_inv_rect_Type2 :
284 monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
285 __ -> __ -> 'a1) -> 'a1
287 val injMonadPred_inv_rect_Type1 :
288 monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
289 __ -> __ -> 'a1) -> 'a1
291 val injMonadPred_inv_rect_Type0 :
292 monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
293 __ -> __ -> 'a1) -> 'a1
295 val injMonadPred_jmdiscr : monad -> injMonadPred -> injMonadPred -> __
300 val monadRel_rect_Type4 :
301 monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
303 val monadRel_rect_Type5 :
304 monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
306 val monadRel_rect_Type3 :
307 monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
309 val monadRel_rect_Type2 :
310 monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
312 val monadRel_rect_Type1 :
313 monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
315 val monadRel_rect_Type0 :
316 monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
318 val monadRel_inv_rect_Type4 :
319 monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
321 val monadRel_inv_rect_Type3 :
322 monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
324 val monadRel_inv_rect_Type2 :
325 monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
327 val monadRel_inv_rect_Type1 :
328 monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
330 val monadRel_inv_rect_Type0 :
331 monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
333 val monadRel_jmdiscr : monad -> monad -> monadRel -> monadRel -> __