extracted/nat.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 Relations
  12
  13 type nat =
  14 | O
  15 | S of nat
  16
  17 val nat_rect_Type4 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1
  18
  19 val nat_rect_Type3 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1
  20
  21 val nat_rect_Type2 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1
  22
  23 val nat_rect_Type1 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1
  24
  25 val nat_rect_Type0 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1
  26
  27 val nat_inv_rect_Type4 :
  28   nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
  29
  30 val nat_inv_rect_Type3 :
  31   nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
  32
  33 val nat_inv_rect_Type2 :
  34   nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
  35
  36 val nat_inv_rect_Type1 :
  37   nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
  38
  39 val nat_inv_rect_Type0 :
  40   nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
  41
  42 val nat_discr : nat -> nat -> __
  43
  44 val pred : nat -> nat
  45
  46 val plus : nat -> nat -> nat
  47
  48 val times : nat -> nat -> nat
  49
  50 val minus : nat -> nat -> nat
  51
  52 open Bool
  53
  54 val eqb : nat -> nat -> Bool.bool
  55
  56 val leb : nat -> nat -> Bool.bool
  57
  58 val min : nat -> nat -> nat
  59
  60 val max : nat -> nat -> nat
  61