helm/software/matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_nat.ml

   1 type nat =
   2 O
   3  | S of nat
   4 ;;
   5
   6 let nat_rec =
   7 (function p -> (function f -> let rec aux =
   8 (function n ->
   9 (match n with
  10    O -> p
  11  | S(n1) -> (f n1 (aux n1)))
  12 ) in aux))
  13 ;;
  14
  15 let nat_rect =
  16 (function p -> (function f -> let rec aux =
  17 (function n ->
  18 (match n with
  19    O -> p
  20  | S(n1) -> (f n1 (aux n1)))
  21 ) in aux))
  22 ;;
  23
  24 let pred =
  25 (function n ->
  26 (match n with
  27    O -> O
  28  | S(p) -> p)
  29 )
  30 ;;
  31