extracted/monad.mli

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Types
  12
  13 open Relations
  14
  15 open Setoids
  16
  17 type ('a, 'b) pred_transformer = __
  18
  19 type ('a, 'b, 'c, 'd) rel_transformer = __
  20
  21 type monad = { m_return : (__ -> __ -> __);
  22                m_bind : (__ -> __ -> __ -> (__ -> __) -> __) }
  23
  24 val monad_rect_Type4 :
  25   (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
  26   monad -> 'a1
  27
  28 val monad_rect_Type5 :
  29   (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
  30   monad -> 'a1
  31
  32 val monad_rect_Type3 :
  33   (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
  34   monad -> 'a1
  35
  36 val monad_rect_Type2 :
  37   (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
  38   monad -> 'a1
  39
  40 val monad_rect_Type1 :
  41   (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
  42   monad -> 'a1
  43
  44 val monad_rect_Type0 :
  45   (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
  46   monad -> 'a1
  47
  48 type 'x_772 monad0
  49
  50 val m_return0 : monad -> 'a1 -> __
  51
  52 val m_bind0 : monad -> __ -> ('a1 -> __) -> __
  53
  54 val monad_inv_rect_Type4 :
  55   monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
  56   __ -> 'a1) -> 'a1
  57
  58 val monad_inv_rect_Type3 :
  59   monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
  60   __ -> 'a1) -> 'a1
  61
  62 val monad_inv_rect_Type2 :
  63   monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
  64   __ -> 'a1) -> 'a1
  65
  66 val monad_inv_rect_Type1 :
  67   monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
  68   __ -> 'a1) -> 'a1
  69
  70 val monad_inv_rect_Type0 :
  71   monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
  72   __ -> 'a1) -> 'a1
  73
  74 type monadProps =
  75   monad
  76   (* singleton inductive, whose constructor was mk_MonadProps *)
  77
  78 val monadProps_rect_Type4 :
  79   (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
  80
  81 val monadProps_rect_Type5 :
  82   (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
  83
  84 val monadProps_rect_Type3 :
  85   (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
  86
  87 val monadProps_rect_Type2 :
  88   (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
  89
  90 val monadProps_rect_Type1 :
  91   (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
  92
  93 val monadProps_rect_Type0 :
  94   (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
  95
  96 val max_def : monadProps -> monad
  97
  98 val monadProps_inv_rect_Type4 :
  99   monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 100
 101 val monadProps_inv_rect_Type3 :
 102   monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 103
 104 val monadProps_inv_rect_Type2 :
 105   monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 106
 107 val monadProps_inv_rect_Type1 :
 108   monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 109
 110 val monadProps_inv_rect_Type0 :
 111   monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 112
 113 type 'x_772 max_def__o__monad = __
 114
 115 type setoidMonadProps =
 116   monad
 117   (* singleton inductive, whose constructor was mk_SetoidMonadProps *)
 118
 119 val setoidMonadProps_rect_Type4 :
 120   (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 121   setoidMonadProps -> 'a1
 122
 123 val setoidMonadProps_rect_Type5 :
 124   (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 125   setoidMonadProps -> 'a1
 126
 127 val setoidMonadProps_rect_Type3 :
 128   (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 129   setoidMonadProps -> 'a1
 130
 131 val setoidMonadProps_rect_Type2 :
 132   (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 133   setoidMonadProps -> 'a1
 134
 135 val setoidMonadProps_rect_Type1 :
 136   (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 137   setoidMonadProps -> 'a1
 138
 139 val setoidMonadProps_rect_Type0 :
 140   (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 141   setoidMonadProps -> 'a1
 142
 143 val smax_def : setoidMonadProps -> monad
 144
 145 val setoidMonadProps_inv_rect_Type4 :
 146   setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 147   -> __ -> __ -> 'a1) -> 'a1
 148
 149 val setoidMonadProps_inv_rect_Type3 :
 150   setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 151   -> __ -> __ -> 'a1) -> 'a1
 152
 153 val setoidMonadProps_inv_rect_Type2 :
 154   setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 155   -> __ -> __ -> 'a1) -> 'a1
 156
 157 val setoidMonadProps_inv_rect_Type1 :
 158   setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 159   -> __ -> __ -> 'a1) -> 'a1
 160
 161 val setoidMonadProps_inv_rect_Type0 :
 162   setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 163   -> __ -> __ -> 'a1) -> 'a1
 164
 165 type 'x_772 smax_def__o__monad = __
 166
 167 val setoid_of_monad : setoidMonadProps -> Setoids.setoid
 168
 169 open Bool
 170
 171 open Nat
 172
 173 open List
 174
 175 val m_map : monad -> ('a1 -> 'a2) -> __ -> __
 176
 177 val m_map2 : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __
 178
 179 val m_bind2 : monad -> __ -> ('a1 -> 'a2 -> __) -> __
 180
 181 val m_bind3 : monad -> __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __
 182
 183 val m_join : monad -> __ -> __
 184
 185 val m_sigbind2 : monad -> __ -> ('a1 -> 'a2 -> __ -> __) -> __
 186
 187 val m_list_map : monad -> ('a1 -> __) -> 'a1 List.list -> __
 188
 189 val m_list_map_sigma : monad -> ('a1 -> __) -> 'a1 List.list -> __
 190
 191 val m_bin_op : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __
 192
 193 val m_fold : monad -> ('a1 -> 'a2 -> __) -> 'a1 List.list -> 'a2 -> __
 194
 195 val makeMonadProps :
 196   (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) -> monadProps
 197
 198 val makeSetoidMonadProps :
 199   (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) ->
 200   setoidMonadProps
 201
 202 open Jmeq
 203
 204 open Russell
 205
 206 type monadPred =
 207 | Mk_MonadPred
 208
 209 val monadPred_rect_Type4 :
 210   monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
 211
 212 val monadPred_rect_Type5 :
 213   monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
 214
 215 val monadPred_rect_Type3 :
 216   monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
 217
 218 val monadPred_rect_Type2 :
 219   monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
 220
 221 val monadPred_rect_Type1 :
 222   monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
 223
 224 val monadPred_rect_Type0 :
 225   monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
 226
 227 val monadPred_inv_rect_Type4 :
 228   monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 229
 230 val monadPred_inv_rect_Type3 :
 231   monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 232
 233 val monadPred_inv_rect_Type2 :
 234   monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 235
 236 val monadPred_inv_rect_Type1 :
 237   monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 238
 239 val monadPred_inv_rect_Type0 :
 240   monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 241
 242 val monadPred_jmdiscr : monad -> monadPred -> monadPred -> __
 243
 244 type injMonadPred = { im_pred : monadPred;
 245                       mp_inject : (__ -> __ -> __ Types.sig0 -> __) }
 246
 247 val injMonadPred_rect_Type4 :
 248   monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
 249   injMonadPred -> 'a1
 250
 251 val injMonadPred_rect_Type5 :
 252   monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
 253   injMonadPred -> 'a1
 254
 255 val injMonadPred_rect_Type3 :
 256   monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
 257   injMonadPred -> 'a1
 258
 259 val injMonadPred_rect_Type2 :
 260   monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
 261   injMonadPred -> 'a1
 262
 263 val injMonadPred_rect_Type1 :
 264   monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
 265   injMonadPred -> 'a1
 266
 267 val injMonadPred_rect_Type0 :
 268   monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
 269   injMonadPred -> 'a1
 270
 271 val im_pred : monad -> injMonadPred -> monadPred
 272
 273 val mp_inject0 : monad -> injMonadPred -> __ Types.sig0 -> __
 274
 275 val injMonadPred_inv_rect_Type4 :
 276   monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
 277   __ -> __ -> 'a1) -> 'a1
 278
 279 val injMonadPred_inv_rect_Type3 :
 280   monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
 281   __ -> __ -> 'a1) -> 'a1
 282
 283 val injMonadPred_inv_rect_Type2 :
 284   monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
 285   __ -> __ -> 'a1) -> 'a1
 286
 287 val injMonadPred_inv_rect_Type1 :
 288   monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
 289   __ -> __ -> 'a1) -> 'a1
 290
 291 val injMonadPred_inv_rect_Type0 :
 292   monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
 293   __ -> __ -> 'a1) -> 'a1
 294
 295 val injMonadPred_jmdiscr : monad -> injMonadPred -> injMonadPred -> __
 296
 297 type monadRel =
 298 | Mk_MonadRel
 299
 300 val monadRel_rect_Type4 :
 301   monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
 302
 303 val monadRel_rect_Type5 :
 304   monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
 305
 306 val monadRel_rect_Type3 :
 307   monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
 308
 309 val monadRel_rect_Type2 :
 310   monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
 311
 312 val monadRel_rect_Type1 :
 313   monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
 314
 315 val monadRel_rect_Type0 :
 316   monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
 317
 318 val monadRel_inv_rect_Type4 :
 319   monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 320
 321 val monadRel_inv_rect_Type3 :
 322   monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 323
 324 val monadRel_inv_rect_Type2 :
 325   monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 326
 327 val monadRel_inv_rect_Type1 :
 328   monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 329
 330 val monadRel_inv_rect_Type0 :
 331   monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 332
 333 val monadRel_jmdiscr : monad -> monad -> monadRel -> monadRel -> __
 334