extracted/positive.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 Bool
  12
  13 open Relations
  14
  15 open Nat
  16
  17 type compare =
  18 | LT
  19 | EQ
  20 | GT
  21
  22 val compare_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
  23
  24 val compare_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
  25
  26 val compare_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
  27
  28 val compare_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
  29
  30 val compare_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
  31
  32 val compare_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
  33
  34 val compare_inv_rect_Type4 :
  35   compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  36
  37 val compare_inv_rect_Type3 :
  38   compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  39
  40 val compare_inv_rect_Type2 :
  41   compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  42
  43 val compare_inv_rect_Type1 :
  44   compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  45
  46 val compare_inv_rect_Type0 :
  47   compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  48
  49 val compare_discr : compare -> compare -> __
  50
  51 val compare_invert : compare -> compare
  52
  53 type pos =
  54 | One
  55 | P1 of pos
  56 | P0 of pos
  57
  58 val pos_rect_Type4 :
  59   'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1
  60
  61 val pos_rect_Type3 :
  62   'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1
  63
  64 val pos_rect_Type2 :
  65   'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1
  66
  67 val pos_rect_Type1 :
  68   'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1
  69
  70 val pos_rect_Type0 :
  71   'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1
  72
  73 val pos_inv_rect_Type4 :
  74   pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
  75   'a1) -> __ -> 'a1) -> 'a1
  76
  77 val pos_inv_rect_Type3 :
  78   pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
  79   'a1) -> __ -> 'a1) -> 'a1
  80
  81 val pos_inv_rect_Type2 :
  82   pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
  83   'a1) -> __ -> 'a1) -> 'a1
  84
  85 val pos_inv_rect_Type1 :
  86   pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
  87   'a1) -> __ -> 'a1) -> 'a1
  88
  89 val pos_inv_rect_Type0 :
  90   pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
  91   'a1) -> __ -> 'a1) -> 'a1
  92
  93 val pos_discr : pos -> pos -> __
  94
  95 val pred : pos -> pos
  96
  97 val succ : pos -> pos
  98
  99 val nat_of_pos : pos -> Nat.nat
 100
 101 val succ_pos_of_nat : Nat.nat -> pos
 102
 103 val plus : pos -> pos -> pos
 104
 105 val times : pos -> pos -> pos
 106
 107 type minusresult =
 108 | MinusNeg
 109 | MinusZero
 110 | MinusPos of pos
 111
 112 val minusresult_rect_Type4 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
 113
 114 val minusresult_rect_Type5 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
 115
 116 val minusresult_rect_Type3 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
 117
 118 val minusresult_rect_Type2 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
 119
 120 val minusresult_rect_Type1 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
 121
 122 val minusresult_rect_Type0 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
 123
 124 val minusresult_inv_rect_Type4 :
 125   minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1
 126
 127 val minusresult_inv_rect_Type3 :
 128   minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1
 129
 130 val minusresult_inv_rect_Type2 :
 131   minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1
 132
 133 val minusresult_inv_rect_Type1 :
 134   minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1
 135
 136 val minusresult_inv_rect_Type0 :
 137   minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1
 138
 139 val minusresult_discr : minusresult -> minusresult -> __
 140
 141 val partial_minus : pos -> pos -> minusresult
 142
 143 val minus : pos -> pos -> pos
 144
 145 val eqb : pos -> pos -> Bool.bool
 146
 147 val eqb_elim : pos -> pos -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 148
 149 val leb : pos -> pos -> Bool.bool
 150
 151 val pos_compare : pos -> pos -> compare
 152
 153 val two_power_nat : Nat.nat -> pos
 154
 155 val two_power_pos : pos -> pos
 156
 157 val max : pos -> pos -> pos
 158