X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_list_list.ml;fp=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_list_list.ml;h=d029b57844411d66d33c573b0c94ab364845a306;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_list_list.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_list_list.ml
new file mode 100644
index 000000000..d029b5784
--- /dev/null
+++ b/matita/contribs/assembly/freescale/freescale_ocaml/matita_list_list.ml
@@ -0,0 +1,74 @@
+type ('a) list =
+Nil
+ | Cons of 'a * ('a) list
+;;
+
+let list_rec =
+(function p -> (function f -> let rec aux = 
+(function l -> 
+(match l with 
+   Nil -> p
+ | Cons(t,l1) -> (f t l1 (aux l1)))
+) in aux))
+;;
+
+let list_rect =
+(function p -> (function f -> let rec aux = 
+(function l -> 
+(match l with 
+   Nil -> p
+ | Cons(t,l1) -> (f t l1 (aux l1)))
+) in aux))
+;;
+
+let id_list =
+let rec id_list = 
+(function l -> 
+(match l with 
+   Nil -> (Nil)
+ | Cons(hd,tl) -> (Cons(hd,(id_list tl))))
+) in id_list
+;;
+
+let append =
+let rec append = 
+(function l1 -> (function l2 -> 
+(match l1 with 
+   Nil -> l2
+ | Cons(hd,tl) -> (Cons(hd,(append tl l2))))
+)) in append
+;;
+
+let tail =
+(function l -> 
+(match l with 
+   Nil -> (Nil)
+ | Cons(hd,tl) -> tl)
+)
+;;
+
+let x1 =
+(Matita_nat_nat.S(Matita_nat_nat.O))
+;;
+
+let x2 =
+(Matita_nat_nat.S(x1))
+;;
+
+let x3 =
+(Matita_nat_nat.S(x2))
+;;
+
+let nth =
+let rec nth = 
+(function l -> (function d -> (function n -> 
+(match n with 
+   Matita_nat_nat.O -> 
+(match l with 
+   Nil -> d
+ | Cons(x,_) -> x)
+
+ | Matita_nat_nat.S(n') -> (nth (tail l) d n'))
+))) in nth
+;;
+