source: driver/extracted/extraMonads.mli @ 3106

Last change on this file since 3106 was 3059, checked in by sacerdot, 7 years ago

New extraction

File size: 5.2 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
52val monadFunctRel_rect_Type4 :
53  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
54  monadFunctRel -> 'a1
55
56val monadFunctRel_rect_Type5 :
57  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
58  monadFunctRel -> 'a1
59
60val monadFunctRel_rect_Type3 :
61  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
62  monadFunctRel -> 'a1
63
64val monadFunctRel_rect_Type2 :
65  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
66  monadFunctRel -> 'a1
67
68val monadFunctRel_rect_Type1 :
69  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
70  monadFunctRel -> 'a1
71
72val monadFunctRel_rect_Type0 :
73  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
74  monadFunctRel -> 'a1
75
76val monadFunctRel_inv_rect_Type4 :
77  Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ -> __
78  -> 'a1) -> 'a1
79
80val monadFunctRel_inv_rect_Type3 :
81  Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ -> __
82  -> 'a1) -> 'a1
83
84val monadFunctRel_inv_rect_Type2 :
85  Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ -> __
86  -> 'a1) -> 'a1
87
88val monadFunctRel_inv_rect_Type1 :
89  Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ -> __
90  -> 'a1) -> 'a1
91
92val monadFunctRel_inv_rect_Type0 :
93  Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ -> __
94  -> 'a1) -> 'a1
95
96val monadFunctRel_jmdiscr :
97  Monad.monad -> Monad.monad -> monadFunctRel -> monadFunctRel -> __
98
99type monadFunctRel1 =
100| Mk_MonadFunctRel1
101
102val monadFunctRel1_rect_Type4 :
103  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
104  monadFunctRel1 -> 'a1
105
106val monadFunctRel1_rect_Type5 :
107  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
108  monadFunctRel1 -> 'a1
109
110val monadFunctRel1_rect_Type3 :
111  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
112  monadFunctRel1 -> 'a1
113
114val monadFunctRel1_rect_Type2 :
115  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
116  monadFunctRel1 -> 'a1
117
118val monadFunctRel1_rect_Type1 :
119  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
120  monadFunctRel1 -> 'a1
121
122val monadFunctRel1_rect_Type0 :
123  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
124  monadFunctRel1 -> 'a1
125
126val monadFunctRel1_inv_rect_Type4 :
127  Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ -> __
128  -> __ -> 'a1) -> 'a1
129
130val monadFunctRel1_inv_rect_Type3 :
131  Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ -> __
132  -> __ -> 'a1) -> 'a1
133
134val monadFunctRel1_inv_rect_Type2 :
135  Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ -> __
136  -> __ -> 'a1) -> 'a1
137
138val monadFunctRel1_inv_rect_Type1 :
139  Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ -> __
140  -> __ -> 'a1) -> 'a1
141
142val monadFunctRel1_inv_rect_Type0 :
143  Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ -> __
144  -> __ -> 'a1) -> 'a1
145
146val monadFunctRel1_jmdiscr :
147  Monad.monad -> Monad.monad -> monadFunctRel1 -> monadFunctRel1 -> __
148
149type monadGenRel =
150| Mk_MonadGenRel
151
152val monadGenRel_rect_Type4 :
153  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
154  monadGenRel -> 'a1
155
156val monadGenRel_rect_Type5 :
157  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
158  monadGenRel -> 'a1
159
160val monadGenRel_rect_Type3 :
161  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
162  monadGenRel -> 'a1
163
164val monadGenRel_rect_Type2 :
165  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
166  monadGenRel -> 'a1
167
168val monadGenRel_rect_Type1 :
169  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
170  monadGenRel -> 'a1
171
172val monadGenRel_rect_Type0 :
173  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
174  monadGenRel -> 'a1
175
176val monadGenRel_inv_rect_Type4 :
177  Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __ ->
178  __ -> 'a1) -> 'a1
179
180val monadGenRel_inv_rect_Type3 :
181  Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __ ->
182  __ -> 'a1) -> 'a1
183
184val monadGenRel_inv_rect_Type2 :
185  Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __ ->
186  __ -> 'a1) -> 'a1
187
188val monadGenRel_inv_rect_Type1 :
189  Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __ ->
190  __ -> 'a1) -> 'a1
191
192val monadGenRel_inv_rect_Type0 :
193  Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __ ->
194  __ -> 'a1) -> 'a1
195
196val monadGenRel_jmdiscr :
197  Monad.monad -> Monad.monad -> monadGenRel -> monadGenRel -> __
198
199val res_preserve : monadFunctRel
200
201val res_preserve1 : monadFunctRel1
202
203val gen_res_preserve : monadGenRel
204
205val opt_preserve : monadFunctRel
206
207val opt_preserve1 : monadFunctRel1
208
209val gen_opt_preserve : monadGenRel
210
211val io_preserve : monadFunctRel
212
213val io_preserve1 : monadFunctRel1
214
215val gen_io_preserve : monadGenRel
216
Note: See TracBrowser for help on using the repository browser.