source: extracted/extraMonads.ml @ 2993

Last change on this file since 2993 was 2829, checked in by sacerdot, 7 years ago

Semantics files committed.

File size: 7.0 KB
Line 
1open Preamble
2
3open ErrorMessages
4
5open Option
6
7open Setoids
8
9open Monad
10
11open Jmeq
12
13open Russell
14
15open Positive
16
17open PreIdentifiers
18
19open Bool
20
21open Relations
22
23open Nat
24
25open List
26
27open Hints_declaration
28
29open Core_notation
30
31open Pts
32
33open Logic
34
35open Types
36
37open Errors
38
39open Proper
40
41open Div_and_mod
42
43open Util
44
45open Extralib
46
47open IOMonad
48
49type monadFunctRel =
50| Mk_MonadFunctRel
51
52(** val monadFunctRel_rect_Type4 :
53    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
54    monadFunctRel -> 'a1 **)
55let rec monadFunctRel_rect_Type4 m1 m2 h_mk_MonadFunctRel = function
56| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
57
58(** val monadFunctRel_rect_Type5 :
59    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
60    monadFunctRel -> 'a1 **)
61let rec monadFunctRel_rect_Type5 m1 m2 h_mk_MonadFunctRel = function
62| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
63
64(** val monadFunctRel_rect_Type3 :
65    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
66    monadFunctRel -> 'a1 **)
67let rec monadFunctRel_rect_Type3 m1 m2 h_mk_MonadFunctRel = function
68| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
69
70(** val monadFunctRel_rect_Type2 :
71    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
72    monadFunctRel -> 'a1 **)
73let rec monadFunctRel_rect_Type2 m1 m2 h_mk_MonadFunctRel = function
74| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
75
76(** val monadFunctRel_rect_Type1 :
77    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
78    monadFunctRel -> 'a1 **)
79let rec monadFunctRel_rect_Type1 m1 m2 h_mk_MonadFunctRel = function
80| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
81
82(** val monadFunctRel_rect_Type0 :
83    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
84    monadFunctRel -> 'a1 **)
85let rec monadFunctRel_rect_Type0 m1 m2 h_mk_MonadFunctRel = function
86| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
87
88(** val monadFunctRel_inv_rect_Type4 :
89    Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
90    __ -> 'a1) -> 'a1 **)
91let monadFunctRel_inv_rect_Type4 x1 x2 hterm h1 =
92  let hcut = monadFunctRel_rect_Type4 x1 x2 h1 hterm in hcut __
93
94(** val monadFunctRel_inv_rect_Type3 :
95    Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
96    __ -> 'a1) -> 'a1 **)
97let monadFunctRel_inv_rect_Type3 x1 x2 hterm h1 =
98  let hcut = monadFunctRel_rect_Type3 x1 x2 h1 hterm in hcut __
99
100(** val monadFunctRel_inv_rect_Type2 :
101    Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
102    __ -> 'a1) -> 'a1 **)
103let monadFunctRel_inv_rect_Type2 x1 x2 hterm h1 =
104  let hcut = monadFunctRel_rect_Type2 x1 x2 h1 hterm in hcut __
105
106(** val monadFunctRel_inv_rect_Type1 :
107    Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
108    __ -> 'a1) -> 'a1 **)
109let monadFunctRel_inv_rect_Type1 x1 x2 hterm h1 =
110  let hcut = monadFunctRel_rect_Type1 x1 x2 h1 hterm in hcut __
111
112(** val monadFunctRel_inv_rect_Type0 :
113    Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
114    __ -> 'a1) -> 'a1 **)
115let monadFunctRel_inv_rect_Type0 x1 x2 hterm h1 =
116  let hcut = monadFunctRel_rect_Type0 x1 x2 h1 hterm in hcut __
117
118(** val monadFunctRel_jmdiscr :
119    Monad.monad -> Monad.monad -> monadFunctRel -> monadFunctRel -> __ **)
120let monadFunctRel_jmdiscr a1 a2 x y =
121  Logic.eq_rect_Type2 x
122    (let Mk_MonadFunctRel = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
123
124type monadFunctRel1 =
125| Mk_MonadFunctRel1
126
127(** val monadFunctRel1_rect_Type4 :
128    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
129    monadFunctRel1 -> 'a1 **)
130let rec monadFunctRel1_rect_Type4 m1 m2 h_mk_MonadFunctRel1 = function
131| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
132
133(** val monadFunctRel1_rect_Type5 :
134    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
135    monadFunctRel1 -> 'a1 **)
136let rec monadFunctRel1_rect_Type5 m1 m2 h_mk_MonadFunctRel1 = function
137| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
138
139(** val monadFunctRel1_rect_Type3 :
140    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
141    monadFunctRel1 -> 'a1 **)
142let rec monadFunctRel1_rect_Type3 m1 m2 h_mk_MonadFunctRel1 = function
143| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
144
145(** val monadFunctRel1_rect_Type2 :
146    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
147    monadFunctRel1 -> 'a1 **)
148let rec monadFunctRel1_rect_Type2 m1 m2 h_mk_MonadFunctRel1 = function
149| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
150
151(** val monadFunctRel1_rect_Type1 :
152    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
153    monadFunctRel1 -> 'a1 **)
154let rec monadFunctRel1_rect_Type1 m1 m2 h_mk_MonadFunctRel1 = function
155| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
156
157(** val monadFunctRel1_rect_Type0 :
158    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
159    monadFunctRel1 -> 'a1 **)
160let rec monadFunctRel1_rect_Type0 m1 m2 h_mk_MonadFunctRel1 = function
161| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
162
163(** val monadFunctRel1_inv_rect_Type4 :
164    Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
165    __ -> __ -> 'a1) -> 'a1 **)
166let monadFunctRel1_inv_rect_Type4 x1 x2 hterm h1 =
167  let hcut = monadFunctRel1_rect_Type4 x1 x2 h1 hterm in hcut __
168
169(** val monadFunctRel1_inv_rect_Type3 :
170    Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
171    __ -> __ -> 'a1) -> 'a1 **)
172let monadFunctRel1_inv_rect_Type3 x1 x2 hterm h1 =
173  let hcut = monadFunctRel1_rect_Type3 x1 x2 h1 hterm in hcut __
174
175(** val monadFunctRel1_inv_rect_Type2 :
176    Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
177    __ -> __ -> 'a1) -> 'a1 **)
178let monadFunctRel1_inv_rect_Type2 x1 x2 hterm h1 =
179  let hcut = monadFunctRel1_rect_Type2 x1 x2 h1 hterm in hcut __
180
181(** val monadFunctRel1_inv_rect_Type1 :
182    Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
183    __ -> __ -> 'a1) -> 'a1 **)
184let monadFunctRel1_inv_rect_Type1 x1 x2 hterm h1 =
185  let hcut = monadFunctRel1_rect_Type1 x1 x2 h1 hterm in hcut __
186
187(** val monadFunctRel1_inv_rect_Type0 :
188    Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
189    __ -> __ -> 'a1) -> 'a1 **)
190let monadFunctRel1_inv_rect_Type0 x1 x2 hterm h1 =
191  let hcut = monadFunctRel1_rect_Type0 x1 x2 h1 hterm in hcut __
192
193(** val monadFunctRel1_jmdiscr :
194    Monad.monad -> Monad.monad -> monadFunctRel1 -> monadFunctRel1 -> __ **)
195let monadFunctRel1_jmdiscr a1 a2 x y =
196  Logic.eq_rect_Type2 x
197    (let Mk_MonadFunctRel1 = x in Obj.magic (fun _ dH -> dH __ __ __ __ __))
198    y
199
200(** val res_preserve : monadFunctRel **)
201let res_preserve =
202  Mk_MonadFunctRel
203
204(** val res_preserve1 : monadFunctRel1 **)
205let res_preserve1 =
206  Mk_MonadFunctRel1
207
208(** val opt_preserve : monadFunctRel **)
209let opt_preserve =
210  Mk_MonadFunctRel
211
212(** val opt_preserve1 : monadFunctRel1 **)
213let opt_preserve1 =
214  Mk_MonadFunctRel1
215
216(** val io_preserve : monadFunctRel **)
217let io_preserve =
218  Mk_MonadFunctRel
219
220(** val io_preserve1 : monadFunctRel1 **)
221let io_preserve1 =
222  Mk_MonadFunctRel1
223
Note: See TracBrowser for help on using the repository browser.