extracted/types.mli

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 type void = unit (* empty inductive *)
  12
  13 val void_rect_Type4 : void -> 'a1
  14
  15 val void_rect_Type5 : void -> 'a1
  16
  17 val void_rect_Type3 : void -> 'a1
  18
  19 val void_rect_Type2 : void -> 'a1
  20
  21 val void_rect_Type1 : void -> 'a1
  22
  23 val void_rect_Type0 : void -> 'a1
  24
  25 type unit0 =
  26 | It
  27
  28 val unit_rect_Type4 : 'a1 -> unit0 -> 'a1
  29
  30 val unit_rect_Type5 : 'a1 -> unit0 -> 'a1
  31
  32 val unit_rect_Type3 : 'a1 -> unit0 -> 'a1
  33
  34 val unit_rect_Type2 : 'a1 -> unit0 -> 'a1
  35
  36 val unit_rect_Type1 : 'a1 -> unit0 -> 'a1
  37
  38 val unit_rect_Type0 : 'a1 -> unit0 -> 'a1
  39
  40 val unit_inv_rect_Type4 : unit0 -> (__ -> 'a1) -> 'a1
  41
  42 val unit_inv_rect_Type3 : unit0 -> (__ -> 'a1) -> 'a1
  43
  44 val unit_inv_rect_Type2 : unit0 -> (__ -> 'a1) -> 'a1
  45
  46 val unit_inv_rect_Type1 : unit0 -> (__ -> 'a1) -> 'a1
  47
  48 val unit_inv_rect_Type0 : unit0 -> (__ -> 'a1) -> 'a1
  49
  50 val unit_discr : unit0 -> unit0 -> __
  51
  52 type ('a, 'b) sum =
  53 | Inl of 'a
  54 | Inr of 'b
  55
  56 val sum_rect_Type4 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
  57
  58 val sum_rect_Type5 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
  59
  60 val sum_rect_Type3 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
  61
  62 val sum_rect_Type2 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
  63
  64 val sum_rect_Type1 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
  65
  66 val sum_rect_Type0 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
  67
  68 val sum_inv_rect_Type4 :
  69   ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3
  70
  71 val sum_inv_rect_Type3 :
  72   ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3
  73
  74 val sum_inv_rect_Type2 :
  75   ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3
  76
  77 val sum_inv_rect_Type1 :
  78   ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3
  79
  80 val sum_inv_rect_Type0 :
  81   ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3
  82
  83 val sum_discr : ('a1, 'a2) sum -> ('a1, 'a2) sum -> __
  84
  85 type 'a option =
  86 | None
  87 | Some of 'a
  88
  89 val option_rect_Type4 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
  90
  91 val option_rect_Type5 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
  92
  93 val option_rect_Type3 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
  94
  95 val option_rect_Type2 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
  96
  97 val option_rect_Type1 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
  98
  99 val option_rect_Type0 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
 100
 101 val option_inv_rect_Type4 :
 102   'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2
 103
 104 val option_inv_rect_Type3 :
 105   'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2
 106
 107 val option_inv_rect_Type2 :
 108   'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2
 109
 110 val option_inv_rect_Type1 :
 111   'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2
 112
 113 val option_inv_rect_Type0 :
 114   'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2
 115
 116 val option_discr : 'a1 option -> 'a1 option -> __
 117
 118 val option_map : ('a1 -> 'a2) -> 'a1 option -> 'a2 option
 119
 120 val option_map_def : ('a1 -> 'a2) -> 'a2 -> 'a1 option -> 'a2
 121
 122 val refute_none_by_refl :
 123   ('a1 -> 'a2) -> 'a1 option -> ('a1 -> __ -> 'a3) -> 'a3
 124
 125 type ('a, 'f) dPair = { dpi1 : 'a; dpi2 : 'f }
 126
 127 val dPair_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
 128
 129 val dPair_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
 130
 131 val dPair_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
 132
 133 val dPair_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
 134
 135 val dPair_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
 136
 137 val dPair_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
 138
 139 val dpi1 : ('a1, 'a2) dPair -> 'a1
 140
 141 val dpi2 : ('a1, 'a2) dPair -> 'a2
 142
 143 val dPair_inv_rect_Type4 :
 144   ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
 145
 146 val dPair_inv_rect_Type3 :
 147   ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
 148
 149 val dPair_inv_rect_Type2 :
 150   ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
 151
 152 val dPair_inv_rect_Type1 :
 153   ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
 154
 155 val dPair_inv_rect_Type0 :
 156   ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
 157
 158 val dPair_discr : ('a1, 'a2) dPair -> ('a1, 'a2) dPair -> __
 159
 160 type 'a sig0 =
 161   'a
 162   (* singleton inductive, whose constructor was mk_Sig *)
 163
 164 val sig_rect_Type4 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
 165
 166 val sig_rect_Type5 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
 167
 168 val sig_rect_Type3 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
 169
 170 val sig_rect_Type2 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
 171
 172 val sig_rect_Type1 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
 173
 174 val sig_rect_Type0 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
 175
 176 val pi1 : 'a1 sig0 -> 'a1
 177
 178 val sig_inv_rect_Type4 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2
 179
 180 val sig_inv_rect_Type3 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2
 181
 182 val sig_inv_rect_Type2 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2
 183
 184 val sig_inv_rect_Type1 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2
 185
 186 val sig_inv_rect_Type0 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2
 187
 188 val sig_discr : 'a1 sig0 -> 'a1 sig0 -> __
 189
 190 type ('a, 'b) prod = { fst : 'a; snd : 'b }
 191
 192 val prod_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
 193
 194 val prod_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
 195
 196 val prod_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
 197
 198 val prod_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
 199
 200 val prod_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
 201
 202 val prod_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
 203
 204 val fst : ('a1, 'a2) prod -> 'a1
 205
 206 val snd : ('a1, 'a2) prod -> 'a2
 207
 208 val prod_inv_rect_Type4 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
 209
 210 val prod_inv_rect_Type3 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
 211
 212 val prod_inv_rect_Type2 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
 213
 214 val prod_inv_rect_Type1 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
 215
 216 val prod_inv_rect_Type0 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
 217
 218 val prod_discr : ('a1, 'a2) prod -> ('a1, 'a2) prod -> __
 219
 220 val coerc_pair_sigma : ('a1, 'a2) prod -> ('a1, 'a2 sig0) prod
 221
 222 val dpi1__o__coerc_pair_sigma :
 223   (('a1, 'a2) prod, 'a3) dPair -> ('a1, 'a2 sig0) prod
 224