source: extracted/extraMonads.mli @ 2829

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

Semantics files committed.

File size: 3.6 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
149val res_preserve : monadFunctRel
150
151val res_preserve1 : monadFunctRel1
152
153val opt_preserve : monadFunctRel
154
155val opt_preserve1 : monadFunctRel1
156
157val io_preserve : monadFunctRel
158
159val io_preserve1 : monadFunctRel1
160
Note: See TracBrowser for help on using the repository browser.