extracted/extraMonads.mli

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