matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_compare.ml

   1 let eqb =
   2 let rec eqb =
   3 (function n -> (function m ->
   4 (match n with
   5    Matita_nat_nat.O ->
   6 (match m with
   7    Matita_nat_nat.O -> Matita_datatypes_bool.True
   8  | Matita_nat_nat.S(q) -> Matita_datatypes_bool.False)
   9
  10  | Matita_nat_nat.S(p) ->
  11 (match m with
  12    Matita_nat_nat.O -> Matita_datatypes_bool.False
  13  | Matita_nat_nat.S(q) -> (eqb p q))
  14 )
  15 )) in eqb
  16 ;;
  17
  18 let leb =
  19 let rec leb =
  20 (function n -> (function m ->
  21 (match n with
  22    Matita_nat_nat.O -> Matita_datatypes_bool.True
  23  | Matita_nat_nat.S(p) ->
  24 (match m with
  25    Matita_nat_nat.O -> Matita_datatypes_bool.False
  26  | Matita_nat_nat.S(q) -> (leb p q))
  27 )
  28 )) in leb
  29 ;;
  30
  31 let ltb =
  32 (function n -> (function m -> (Matita_datatypes_bool.andb (leb n m) (Matita_datatypes_bool.notb (eqb n m)))))
  33 ;;
  34
  35 let nat_compare =
  36 let rec nat_compare =
  37 (function n -> (function m ->
  38 (match n with
  39    Matita_nat_nat.O ->
  40 (match m with
  41    Matita_nat_nat.O -> Matita_datatypes_compare.EQ
  42  | Matita_nat_nat.S(q) -> Matita_datatypes_compare.LT)
  43
  44  | Matita_nat_nat.S(p) ->
  45 (match m with
  46    Matita_nat_nat.O -> Matita_datatypes_compare.GT
  47  | Matita_nat_nat.S(q) -> (nat_compare p q))
  48 )
  49 )) in nat_compare
  50 ;;
  51