27 open Hints_declaration
52 (** val monadFunctRel_rect_Type4 :
53 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
54 monadFunctRel -> 'a1 **)
55 let rec monadFunctRel_rect_Type4 m1 m2 h_mk_MonadFunctRel = function
56 | Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
58 (** val monadFunctRel_rect_Type5 :
59 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
60 monadFunctRel -> 'a1 **)
61 let rec monadFunctRel_rect_Type5 m1 m2 h_mk_MonadFunctRel = function
62 | Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
64 (** val monadFunctRel_rect_Type3 :
65 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
66 monadFunctRel -> 'a1 **)
67 let rec monadFunctRel_rect_Type3 m1 m2 h_mk_MonadFunctRel = function
68 | Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
70 (** val monadFunctRel_rect_Type2 :
71 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
72 monadFunctRel -> 'a1 **)
73 let rec monadFunctRel_rect_Type2 m1 m2 h_mk_MonadFunctRel = function
74 | Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
76 (** val monadFunctRel_rect_Type1 :
77 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
78 monadFunctRel -> 'a1 **)
79 let rec monadFunctRel_rect_Type1 m1 m2 h_mk_MonadFunctRel = function
80 | Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
82 (** val monadFunctRel_rect_Type0 :
83 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
84 monadFunctRel -> 'a1 **)
85 let rec monadFunctRel_rect_Type0 m1 m2 h_mk_MonadFunctRel = function
86 | Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
88 (** val monadFunctRel_inv_rect_Type4 :
89 Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
91 let monadFunctRel_inv_rect_Type4 x1 x2 hterm h1 =
92 let hcut = monadFunctRel_rect_Type4 x1 x2 h1 hterm in hcut __
94 (** val monadFunctRel_inv_rect_Type3 :
95 Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
97 let monadFunctRel_inv_rect_Type3 x1 x2 hterm h1 =
98 let hcut = monadFunctRel_rect_Type3 x1 x2 h1 hterm in hcut __
100 (** val monadFunctRel_inv_rect_Type2 :
101 Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
102 __ -> 'a1) -> 'a1 **)
103 let monadFunctRel_inv_rect_Type2 x1 x2 hterm h1 =
104 let hcut = monadFunctRel_rect_Type2 x1 x2 h1 hterm in hcut __
106 (** val monadFunctRel_inv_rect_Type1 :
107 Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
108 __ -> 'a1) -> 'a1 **)
109 let monadFunctRel_inv_rect_Type1 x1 x2 hterm h1 =
110 let hcut = monadFunctRel_rect_Type1 x1 x2 h1 hterm in hcut __
112 (** val monadFunctRel_inv_rect_Type0 :
113 Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
114 __ -> 'a1) -> 'a1 **)
115 let monadFunctRel_inv_rect_Type0 x1 x2 hterm h1 =
116 let hcut = monadFunctRel_rect_Type0 x1 x2 h1 hterm in hcut __
118 (** val monadFunctRel_jmdiscr :
119 Monad.monad -> Monad.monad -> monadFunctRel -> monadFunctRel -> __ **)
120 let monadFunctRel_jmdiscr a1 a2 x y =
121 Logic.eq_rect_Type2 x
122 (let Mk_MonadFunctRel = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
124 type monadFunctRel1 =
127 (** val monadFunctRel1_rect_Type4 :
128 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
129 monadFunctRel1 -> 'a1 **)
130 let rec monadFunctRel1_rect_Type4 m1 m2 h_mk_MonadFunctRel1 = function
131 | Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
133 (** val monadFunctRel1_rect_Type5 :
134 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
135 monadFunctRel1 -> 'a1 **)
136 let rec monadFunctRel1_rect_Type5 m1 m2 h_mk_MonadFunctRel1 = function
137 | Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
139 (** val monadFunctRel1_rect_Type3 :
140 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
141 monadFunctRel1 -> 'a1 **)
142 let rec monadFunctRel1_rect_Type3 m1 m2 h_mk_MonadFunctRel1 = function
143 | Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
145 (** val monadFunctRel1_rect_Type2 :
146 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
147 monadFunctRel1 -> 'a1 **)
148 let rec monadFunctRel1_rect_Type2 m1 m2 h_mk_MonadFunctRel1 = function
149 | Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
151 (** val monadFunctRel1_rect_Type1 :
152 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
153 monadFunctRel1 -> 'a1 **)
154 let rec monadFunctRel1_rect_Type1 m1 m2 h_mk_MonadFunctRel1 = function
155 | Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
157 (** val monadFunctRel1_rect_Type0 :
158 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
159 monadFunctRel1 -> 'a1 **)
160 let rec monadFunctRel1_rect_Type0 m1 m2 h_mk_MonadFunctRel1 = function
161 | Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
163 (** val monadFunctRel1_inv_rect_Type4 :
164 Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
165 __ -> __ -> 'a1) -> 'a1 **)
166 let monadFunctRel1_inv_rect_Type4 x1 x2 hterm h1 =
167 let hcut = monadFunctRel1_rect_Type4 x1 x2 h1 hterm in hcut __
169 (** val monadFunctRel1_inv_rect_Type3 :
170 Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
171 __ -> __ -> 'a1) -> 'a1 **)
172 let monadFunctRel1_inv_rect_Type3 x1 x2 hterm h1 =
173 let hcut = monadFunctRel1_rect_Type3 x1 x2 h1 hterm in hcut __
175 (** val monadFunctRel1_inv_rect_Type2 :
176 Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
177 __ -> __ -> 'a1) -> 'a1 **)
178 let monadFunctRel1_inv_rect_Type2 x1 x2 hterm h1 =
179 let hcut = monadFunctRel1_rect_Type2 x1 x2 h1 hterm in hcut __
181 (** val monadFunctRel1_inv_rect_Type1 :
182 Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
183 __ -> __ -> 'a1) -> 'a1 **)
184 let monadFunctRel1_inv_rect_Type1 x1 x2 hterm h1 =
185 let hcut = monadFunctRel1_rect_Type1 x1 x2 h1 hterm in hcut __
187 (** val monadFunctRel1_inv_rect_Type0 :
188 Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
189 __ -> __ -> 'a1) -> 'a1 **)
190 let monadFunctRel1_inv_rect_Type0 x1 x2 hterm h1 =
191 let hcut = monadFunctRel1_rect_Type0 x1 x2 h1 hterm in hcut __
193 (** val monadFunctRel1_jmdiscr :
194 Monad.monad -> Monad.monad -> monadFunctRel1 -> monadFunctRel1 -> __ **)
195 let monadFunctRel1_jmdiscr a1 a2 x y =
196 Logic.eq_rect_Type2 x
197 (let Mk_MonadFunctRel1 = x in Obj.magic (fun _ dH -> dH __ __ __ __ __))
203 (** val monadGenRel_rect_Type4 :
204 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
205 monadGenRel -> 'a1 **)
206 let rec monadGenRel_rect_Type4 m1 m2 h_mk_MonadGenRel = function
207 | Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
209 (** val monadGenRel_rect_Type5 :
210 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
211 monadGenRel -> 'a1 **)
212 let rec monadGenRel_rect_Type5 m1 m2 h_mk_MonadGenRel = function
213 | Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
215 (** val monadGenRel_rect_Type3 :
216 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
217 monadGenRel -> 'a1 **)
218 let rec monadGenRel_rect_Type3 m1 m2 h_mk_MonadGenRel = function
219 | Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
221 (** val monadGenRel_rect_Type2 :
222 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
223 monadGenRel -> 'a1 **)
224 let rec monadGenRel_rect_Type2 m1 m2 h_mk_MonadGenRel = function
225 | Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
227 (** val monadGenRel_rect_Type1 :
228 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
229 monadGenRel -> 'a1 **)
230 let rec monadGenRel_rect_Type1 m1 m2 h_mk_MonadGenRel = function
231 | Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
233 (** val monadGenRel_rect_Type0 :
234 Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
235 monadGenRel -> 'a1 **)
236 let rec monadGenRel_rect_Type0 m1 m2 h_mk_MonadGenRel = function
237 | Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
239 (** val monadGenRel_inv_rect_Type4 :
240 Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
241 -> __ -> 'a1) -> 'a1 **)
242 let monadGenRel_inv_rect_Type4 x1 x2 hterm h1 =
243 let hcut = monadGenRel_rect_Type4 x1 x2 h1 hterm in hcut __
245 (** val monadGenRel_inv_rect_Type3 :
246 Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
247 -> __ -> 'a1) -> 'a1 **)
248 let monadGenRel_inv_rect_Type3 x1 x2 hterm h1 =
249 let hcut = monadGenRel_rect_Type3 x1 x2 h1 hterm in hcut __
251 (** val monadGenRel_inv_rect_Type2 :
252 Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
253 -> __ -> 'a1) -> 'a1 **)
254 let monadGenRel_inv_rect_Type2 x1 x2 hterm h1 =
255 let hcut = monadGenRel_rect_Type2 x1 x2 h1 hterm in hcut __
257 (** val monadGenRel_inv_rect_Type1 :
258 Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
259 -> __ -> 'a1) -> 'a1 **)
260 let monadGenRel_inv_rect_Type1 x1 x2 hterm h1 =
261 let hcut = monadGenRel_rect_Type1 x1 x2 h1 hterm in hcut __
263 (** val monadGenRel_inv_rect_Type0 :
264 Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
265 -> __ -> 'a1) -> 'a1 **)
266 let monadGenRel_inv_rect_Type0 x1 x2 hterm h1 =
267 let hcut = monadGenRel_rect_Type0 x1 x2 h1 hterm in hcut __
269 (** val monadGenRel_jmdiscr :
270 Monad.monad -> Monad.monad -> monadGenRel -> monadGenRel -> __ **)
271 let monadGenRel_jmdiscr a1 a2 x y =
272 Logic.eq_rect_Type2 x
273 (let Mk_MonadGenRel = x in Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
275 (** val res_preserve : monadFunctRel **)
279 (** val res_preserve1 : monadFunctRel1 **)
283 (** val gen_res_preserve : monadGenRel **)
284 let gen_res_preserve =
287 (** val opt_preserve : monadFunctRel **)
291 (** val opt_preserve1 : monadFunctRel1 **)
295 (** val gen_opt_preserve : monadGenRel **)
296 let gen_opt_preserve =
299 (** val io_preserve : monadFunctRel **)
303 (** val io_preserve1 : monadFunctRel1 **)
307 (** val gen_io_preserve : monadGenRel **)
308 let gen_io_preserve =