extracted/z.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 Positive
  18
  19 type z =
  20 | OZ
  21 | Pos of Positive.pos
  22 | Neg of Positive.pos
  23
  24 val z_rect_Type4 :
  25   'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
  26
  27 val z_rect_Type5 :
  28   'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
  29
  30 val z_rect_Type3 :
  31   'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
  32
  33 val z_rect_Type2 :
  34   'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
  35
  36 val z_rect_Type1 :
  37   'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
  38
  39 val z_rect_Type0 :
  40   'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
  41
  42 val z_inv_rect_Type4 :
  43   z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
  44   'a1) -> 'a1
  45
  46 val z_inv_rect_Type3 :
  47   z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
  48   'a1) -> 'a1
  49
  50 val z_inv_rect_Type2 :
  51   z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
  52   'a1) -> 'a1
  53
  54 val z_inv_rect_Type1 :
  55   z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
  56   'a1) -> 'a1
  57
  58 val z_inv_rect_Type0 :
  59   z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
  60   'a1) -> 'a1
  61
  62 val z_discr : z -> z -> __
  63
  64 val z_of_nat : Nat.nat -> z
  65
  66 val neg_Z_of_nat : Nat.nat -> z
  67
  68 val abs : z -> Nat.nat
  69
  70 val oZ_test : z -> Bool.bool
  71
  72 val zsucc : z -> z
  73
  74 val zpred : z -> z
  75
  76 val eqZb : z -> z -> Bool.bool
  77
  78 val z_compare : z -> z -> Positive.compare
  79
  80 val zplus : z -> z -> z
  81
  82 val zopp : z -> z
  83
  84 val zminus : z -> z -> z
  85
  86 val z_two_power_nat : Nat.nat -> z
  87
  88 val z_two_power_pos : Positive.pos -> z
  89
  90 val two_p : z -> z
  91
  92 open Types
  93
  94 val decidable_eq_Z_Type : z -> z -> (__, __) Types.sum
  95
  96 val zleb : z -> z -> Bool.bool
  97
  98 val zltb : z -> z -> Bool.bool
  99
 100 val zleb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 101
 102 val zltb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 103
 104 val z_times : z -> z -> z
 105
 106 val zmax : z -> z -> z
 107