]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_nat.ml
dfefaeb2dcfc2344f4e0733554c7ef6f8b213bbd
[helm.git] / 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