extracted/nat.ml

   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 let rec nat_rect_Type4 h_O h_S = function
  19 | O -> h_O
  20 | S x_565 -> h_S x_565 (nat_rect_Type4 h_O h_S x_565)
  21
  22 (** val nat_rect_Type3 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
  23 let rec nat_rect_Type3 h_O h_S = function
  24 | O -> h_O
  25 | S x_573 -> h_S x_573 (nat_rect_Type3 h_O h_S x_573)
  26
  27 (** val nat_rect_Type2 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
  28 let rec nat_rect_Type2 h_O h_S = function
  29 | O -> h_O
  30 | S x_577 -> h_S x_577 (nat_rect_Type2 h_O h_S x_577)
  31
  32 (** val nat_rect_Type1 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
  33 let rec nat_rect_Type1 h_O h_S = function
  34 | O -> h_O
  35 | S x_581 -> h_S x_581 (nat_rect_Type1 h_O h_S x_581)
  36
  37 (** val nat_rect_Type0 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
  38 let rec nat_rect_Type0 h_O h_S = function
  39 | O -> h_O
  40 | S x_585 -> h_S x_585 (nat_rect_Type0 h_O h_S x_585)
  41
  42 (** val nat_inv_rect_Type4 :
  43     nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
  44 let nat_inv_rect_Type4 hterm h1 h2 =
  45   let hcut = nat_rect_Type4 h1 h2 hterm in hcut __
  46
  47 (** val nat_inv_rect_Type3 :
  48     nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
  49 let nat_inv_rect_Type3 hterm h1 h2 =
  50   let hcut = nat_rect_Type3 h1 h2 hterm in hcut __
  51
  52 (** val nat_inv_rect_Type2 :
  53     nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
  54 let nat_inv_rect_Type2 hterm h1 h2 =
  55   let hcut = nat_rect_Type2 h1 h2 hterm in hcut __
  56
  57 (** val nat_inv_rect_Type1 :
  58     nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
  59 let nat_inv_rect_Type1 hterm h1 h2 =
  60   let hcut = nat_rect_Type1 h1 h2 hterm in hcut __
  61
  62 (** val nat_inv_rect_Type0 :
  63     nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
  64 let nat_inv_rect_Type0 hterm h1 h2 =
  65   let hcut = nat_rect_Type0 h1 h2 hterm in hcut __
  66
  67 (** val nat_discr : nat -> nat -> __ **)
  68 let nat_discr x y =
  69   Logic.eq_rect_Type2 x
  70     (match x with
  71      | O -> Obj.magic (fun _ dH -> dH)
  72      | S a0 -> Obj.magic (fun _ dH -> dH __)) y
  73
  74 (** val pred : nat -> nat **)
  75 let pred = function
  76 | O -> O
  77 | S p -> p
  78
  79 (** val plus : nat -> nat -> nat **)
  80 let rec plus n m =
  81   match n with
  82   | O -> m
  83   | S p -> S (plus p m)
  84
  85 (** val times : nat -> nat -> nat **)
  86 let rec times n m =
  87   match n with
  88   | O -> O
  89   | S p -> plus m (times p m)
  90
  91 (** val minus : nat -> nat -> nat **)
  92 let rec minus n m =
  93   match n with
  94   | O -> O
  95   | S p ->
  96     (match m with
  97      | O -> S p
  98      | S q -> minus p q)
  99
 100 open Bool
 101
 102 (** val eqb : nat -> nat -> Bool.bool **)
 103 let rec eqb n m =
 104   match n with
 105   | O ->
 106     (match m with
 107      | O -> Bool.True
 108      | S q -> Bool.False)
 109   | S p ->
 110     (match m with
 111      | O -> Bool.False
 112      | S q -> eqb p q)
 113
 114 (** val leb : nat -> nat -> Bool.bool **)
 115 let rec leb n m =
 116   match n with
 117   | O -> Bool.True
 118   | S p ->
 119     (match m with
 120      | O -> Bool.False
 121      | S q -> leb p q)
 122
 123 (** val min : nat -> nat -> nat **)
 124 let min n m =
 125   match leb n m with
 126   | Bool.True -> n
 127   | Bool.False -> m
 128
 129 (** val max : nat -> nat -> nat **)
 130 let max n m =
 131   match leb n m with
 132   | Bool.True -> m
 133   | Bool.False -> n
 134