extracted/bigops.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 Bool
  14
  15 open Relations
  16
  17 open Nat
  18
  19 open Div_and_mod
  20
  21 val prodF :
  22   (Nat.nat -> 'a1) -> (Nat.nat -> 'a2) -> Nat.nat -> Nat.nat -> ('a1, 'a2)
  23   Types.prod
  24
  25 val bigop :
  26   Nat.nat -> (Nat.nat -> Bool.bool) -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> (Nat.nat
  27   -> 'a1) -> 'a1
  28
  29 type 'a aop =
  30   'a -> 'a -> 'a
  31   (* singleton inductive, whose constructor was mk_Aop *)
  32
  33 val aop_rect_Type4 :
  34   'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
  35
  36 val aop_rect_Type5 :
  37   'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
  38
  39 val aop_rect_Type3 :
  40   'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
  41
  42 val aop_rect_Type2 :
  43   'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
  44
  45 val aop_rect_Type1 :
  46   'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
  47
  48 val aop_rect_Type0 :
  49   'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
  50
  51 val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1
  52
  53 val aop_inv_rect_Type4 :
  54   'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
  55   'a2
  56
  57 val aop_inv_rect_Type3 :
  58   'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
  59   'a2
  60
  61 val aop_inv_rect_Type2 :
  62   'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
  63   'a2
  64
  65 val aop_inv_rect_Type1 :
  66   'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
  67   'a2
  68
  69 val aop_inv_rect_Type0 :
  70   'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
  71   'a2
  72
  73 val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __
  74
  75 val dpi1__o__op : 'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1
  76
  77 type 'a aCop =
  78   'a aop
  79   (* singleton inductive, whose constructor was mk_ACop *)
  80
  81 val aCop_rect_Type4 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
  82
  83 val aCop_rect_Type5 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
  84
  85 val aCop_rect_Type3 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
  86
  87 val aCop_rect_Type2 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
  88
  89 val aCop_rect_Type1 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
  90
  91 val aCop_rect_Type0 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
  92
  93 val aop0 : 'a1 -> 'a1 aCop -> 'a1 aop
  94
  95 val aCop_inv_rect_Type4 :
  96   'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2
  97
  98 val aCop_inv_rect_Type3 :
  99   'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2
 100
 101 val aCop_inv_rect_Type2 :
 102   'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2
 103
 104 val aCop_inv_rect_Type1 :
 105   'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2
 106
 107 val aCop_inv_rect_Type0 :
 108   'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2
 109
 110 val aCop_discr : 'a1 -> 'a1 aCop -> 'a1 aCop -> __
 111
 112 val dpi1__o__aop__o__op :
 113   'a1 -> ('a1 aCop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1
 114
 115 val aop__o__op : 'a1 -> 'a1 aCop -> 'a1 -> 'a1 -> 'a1
 116
 117 val dpi1__o__aop : 'a1 -> ('a1 aCop, 'a2) Types.dPair -> 'a1 aop
 118
 119 type 'a range = { enum : (Nat.nat -> 'a); upto : Nat.nat;
 120                   filter : (Nat.nat -> Bool.bool) }
 121
 122 val range_rect_Type4 :
 123   ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
 124   -> 'a2
 125
 126 val range_rect_Type5 :
 127   ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
 128   -> 'a2
 129
 130 val range_rect_Type3 :
 131   ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
 132   -> 'a2
 133
 134 val range_rect_Type2 :
 135   ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
 136   -> 'a2
 137
 138 val range_rect_Type1 :
 139   ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
 140   -> 'a2
 141
 142 val range_rect_Type0 :
 143   ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
 144   -> 'a2
 145
 146 val enum : 'a1 range -> Nat.nat -> 'a1
 147
 148 val upto : 'a1 range -> Nat.nat
 149
 150 val filter : 'a1 range -> Nat.nat -> Bool.bool
 151
 152 val range_inv_rect_Type4 :
 153   'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
 154   -> 'a2) -> 'a2
 155
 156 val range_inv_rect_Type3 :
 157   'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
 158   -> 'a2) -> 'a2
 159
 160 val range_inv_rect_Type2 :
 161   'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
 162   -> 'a2) -> 'a2
 163
 164 val range_inv_rect_Type1 :
 165   'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
 166   -> 'a2) -> 'a2
 167
 168 val range_inv_rect_Type0 :
 169   'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
 170   -> 'a2) -> 'a2
 171
 172 val range_discr : 'a1 range -> 'a1 range -> __
 173
 174 type 'a dop = { sum0 : 'a aCop; prod0 : ('a -> 'a -> 'a) }
 175
 176 val dop_rect_Type4 :
 177   'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
 178   'a2
 179
 180 val dop_rect_Type5 :
 181   'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
 182   'a2
 183
 184 val dop_rect_Type3 :
 185   'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
 186   'a2
 187
 188 val dop_rect_Type2 :
 189   'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
 190   'a2
 191
 192 val dop_rect_Type1 :
 193   'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
 194   'a2
 195
 196 val dop_rect_Type0 :
 197   'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
 198   'a2
 199
 200 val sum0 : 'a1 -> 'a1 dop -> 'a1 aCop
 201
 202 val prod0 : 'a1 -> 'a1 dop -> 'a1 -> 'a1 -> 'a1
 203
 204 val dop_inv_rect_Type4 :
 205   'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
 206   'a2) -> 'a2
 207
 208 val dop_inv_rect_Type3 :
 209   'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
 210   'a2) -> 'a2
 211
 212 val dop_inv_rect_Type2 :
 213   'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
 214   'a2) -> 'a2
 215
 216 val dop_inv_rect_Type1 :
 217   'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
 218   'a2) -> 'a2
 219
 220 val dop_inv_rect_Type0 :
 221   'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
 222   'a2) -> 'a2
 223
 224 val dop_discr : 'a1 -> 'a1 dop -> 'a1 dop -> __
 225