extracted/division.mli

   1 open Preamble
   2
   3 open Types
   4
   5 open Bool
   6
   7 open Relations
   8
   9 open Nat
  10
  11 open Hints_declaration
  12
  13 open Core_notation
  14
  15 open Pts
  16
  17 open Logic
  18
  19 open Positive
  20
  21 open Z
  22
  23 type natp =
  24 | Pzero
  25 | Ppos of Positive.pos
  26
  27 val natp_rect_Type4 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
  28
  29 val natp_rect_Type5 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
  30
  31 val natp_rect_Type3 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
  32
  33 val natp_rect_Type2 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
  34
  35 val natp_rect_Type1 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
  36
  37 val natp_rect_Type0 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
  38
  39 val natp_inv_rect_Type4 :
  40   natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1
  41
  42 val natp_inv_rect_Type3 :
  43   natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1
  44
  45 val natp_inv_rect_Type2 :
  46   natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1
  47
  48 val natp_inv_rect_Type1 :
  49   natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1
  50
  51 val natp_inv_rect_Type0 :
  52   natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1
  53
  54 val natp_discr : natp -> natp -> __
  55
  56 val natp0 : natp -> natp
  57
  58 val natp1 : natp -> natp
  59
  60 val divide : Positive.pos -> Positive.pos -> (natp, natp) Types.prod
  61
  62 val div : Positive.pos -> Positive.pos -> natp
  63
  64 val mod0 : Positive.pos -> Positive.pos -> natp
  65
  66 val natp_plus : natp -> natp -> natp
  67
  68 val natp_times : natp -> natp -> natp
  69
  70 val dec_divides : Positive.pos -> Positive.pos -> (__, __) Types.sum
  71
  72 val dec_dividesZ : Z.z -> Z.z -> (__, __) Types.sum
  73
  74 val natp_to_Z : natp -> Z.z
  75
  76 val natp_to_negZ : natp -> Z.z
  77
  78 val divZ : Z.z -> Z.z -> Z.z
  79
  80 val modZ : Z.z -> Z.z -> Z.z
  81