extracted/util.mli

   1 open Preamble
   2
   3 open Bool
   4
   5 open Relations
   6
   7 open Nat
   8
   9 open Hints_declaration
  10
  11 open Core_notation
  12
  13 open Pts
  14
  15 open Logic
  16
  17 open Types
  18
  19 open List
  20
  21 open Jmeq
  22
  23 open Russell
  24
  25 type dAEMONXXX =
  26 | K1DAEMONXXX
  27 | K2DAEMONXXX
  28
  29 val dAEMONXXX_rect_Type4 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
  30
  31 val dAEMONXXX_rect_Type5 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
  32
  33 val dAEMONXXX_rect_Type3 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
  34
  35 val dAEMONXXX_rect_Type2 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
  36
  37 val dAEMONXXX_rect_Type1 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
  38
  39 val dAEMONXXX_rect_Type0 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
  40
  41 val dAEMONXXX_inv_rect_Type4 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  42
  43 val dAEMONXXX_inv_rect_Type3 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  44
  45 val dAEMONXXX_inv_rect_Type2 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  46
  47 val dAEMONXXX_inv_rect_Type1 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  48
  49 val dAEMONXXX_inv_rect_Type0 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  50
  51 val dAEMONXXX_discr : dAEMONXXX -> dAEMONXXX -> __
  52
  53 val dAEMONXXX_jmdiscr : dAEMONXXX -> dAEMONXXX -> __
  54
  55 val ltb : Nat.nat -> Nat.nat -> Bool.bool
  56
  57 val geb : Nat.nat -> Nat.nat -> Bool.bool
  58
  59 val gtb : Nat.nat -> Nat.nat -> Bool.bool
  60
  61 val eq_nat : Nat.nat -> Nat.nat -> Bool.bool
  62
  63 val forall : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool
  64
  65 val prefix : Nat.nat -> 'a1 List.list -> 'a1 List.list
  66
  67 val fold_left2 :
  68   ('a1 -> 'a2 -> 'a3 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a3 List.list -> 'a1
  69
  70 val remove_n_first_internal :
  71   Nat.nat -> 'a1 List.list -> Nat.nat -> 'a1 List.list
  72
  73 val remove_n_first : Nat.nat -> 'a1 List.list -> 'a1 List.list
  74
  75 val foldi_from_until_internal :
  76   Nat.nat -> 'a1 List.list -> 'a1 List.list -> Nat.nat -> (Nat.nat -> 'a1
  77   List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list
  78
  79 val foldi_from_until :
  80   Nat.nat -> Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) ->
  81   'a1 List.list -> 'a1 List.list -> 'a1 List.list
  82
  83 val foldi_from :
  84   Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
  85   List.list -> 'a1 List.list -> 'a1 List.list
  86
  87 val foldi_until :
  88   Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
  89   List.list -> 'a1 List.list -> 'a1 List.list
  90
  91 val foldi :
  92   (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list -> 'a1
  93   List.list -> 'a1 List.list
  94
  95 val hd_safe : 'a1 List.list -> 'a1
  96
  97 val tail_safe : 'a1 List.list -> 'a1 List.list
  98
  99 val safe_split :
 100   'a1 List.list -> Nat.nat -> ('a1 List.list, 'a1 List.list) Types.prod
 101
 102 val nth_safe : Nat.nat -> 'a1 List.list -> 'a1
 103
 104 val last_safe : 'a1 List.list -> 'a1
 105
 106 val reduce :
 107   'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
 108   Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod
 109
 110 val reduce_strong :
 111   'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
 112   Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod
 113   Types.sig0
 114
 115 val map2_opt :
 116   ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list
 117   Types.option
 118
 119 val map2 :
 120   ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list
 121
 122 val map3 :
 123   ('a1 -> 'a2 -> 'a3 -> 'a4) -> 'a1 List.list -> 'a2 List.list -> 'a3
 124   List.list -> 'a4 List.list
 125
 126 val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2
 127
 128 val safe_nth : Nat.nat -> 'a1 List.list -> 'a1
 129
 130 val nub_by_internal :
 131   ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat -> 'a1 List.list
 132
 133 val nub_by : ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list
 134
 135 val member : ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> Bool.bool
 136
 137 val take : Nat.nat -> 'a1 List.list -> 'a1 List.list
 138
 139 val drop : Nat.nat -> 'a1 List.list -> 'a1 List.list
 140
 141 val list_split :
 142   Nat.nat -> 'a1 List.list -> ('a1 List.list, 'a1 List.list) Types.prod
 143
 144 val mapi_internal :
 145   Nat.nat -> (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list
 146
 147 val mapi : (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list
 148
 149 val zip_pottier :
 150   'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
 151
 152 val zip_safe :
 153   'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
 154
 155 val zip :
 156   'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
 157   Types.option
 158
 159 val foldl : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1
 160
 161 val rev : 'a1 List.list -> 'a1 List.list
 162
 163 val fold_left_i_aux :
 164   (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> Nat.nat -> 'a2 List.list -> 'a1
 165
 166 val fold_left_i :
 167   (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1
 168
 169 val function_apply : ('a1 -> 'a2) -> 'a1 -> 'a2
 170
 171 val iterate : ('a1 -> 'a1) -> 'a1 -> Nat.nat -> 'a1
 172
 173 val division_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat
 174
 175 val division : Nat.nat -> Nat.nat -> Nat.nat
 176
 177 val modulus_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat
 178
 179 val modulus : Nat.nat -> Nat.nat -> Nat.nat
 180
 181 val divide_with_remainder :
 182   Nat.nat -> Nat.nat -> (Nat.nat, Nat.nat) Types.prod
 183
 184 val less_than_or_equal_b_elim :
 185   Nat.nat -> Nat.nat -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 186
 187 open Div_and_mod
 188
 189 val dpi1__o__bool_to_Prop__o__inject :
 190   (Bool.bool, 'a1) Types.dPair -> __ Types.sig0
 191
 192 val eject__o__bool_to_Prop__o__inject : Bool.bool Types.sig0 -> __ Types.sig0
 193
 194 val bool_to_Prop__o__inject : Bool.bool -> __ Types.sig0
 195
 196 val dpi1__o__bool_to_Prop_to_eq__o__inject :
 197   Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0
 198
 199 val eject__o__bool_to_Prop_to_eq__o__inject :
 200   Bool.bool -> __ Types.sig0 -> __ Types.sig0
 201
 202 val bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0
 203
 204 val dpi1__o__not_bool_to_Prop_to_eq__o__inject :
 205   Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0
 206
 207 val eject__o__not_bool_to_Prop_to_eq__o__inject :
 208   Bool.bool -> __ Types.sig0 -> __ Types.sig0
 209
 210 val not_bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0
 211
 212 val if_then_else_safe : Bool.bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 213
 214 val dpi1__o__not_neq_None__o__inject :
 215   'a1 Types.option -> (__, 'a2) Types.dPair -> __ Types.sig0
 216
 217 val eject__o__not_neq_None__o__inject :
 218   'a1 Types.option -> __ Types.sig0 -> __ Types.sig0
 219
 220 val not_neq_None__o__inject : 'a1 Types.option -> __ Types.sig0
 221
 222 val prod_jmdiscr : ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __
 223
 224 val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2
 225
 226 val some_Some_elim : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2
 227
 228 val pose : 'a1 -> ('a1 -> __ -> 'a2) -> 'a2
 229
 230 val eq_sum :
 231   ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
 232   Types.sum -> ('a1, 'a2) Types.sum -> Bool.bool
 233
 234 val eq_prod :
 235   ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
 236   Types.prod -> ('a1, 'a2) Types.prod -> Bool.bool
 237