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

   1 type ('a) list =
   2 Nil
   3  | Cons of 'a * ('a) list
   4 ;;
   5
   6 let list_rec =
   7 (function p -> (function f -> let rec aux =
   8 (function l ->
   9 (match l with
  10    Nil -> p
  11  | Cons(t,l1) -> (f t l1 (aux l1)))
  12 ) in aux))
  13 ;;
  14
  15 let list_rect =
  16 (function p -> (function f -> let rec aux =
  17 (function l ->
  18 (match l with
  19    Nil -> p
  20  | Cons(t,l1) -> (f t l1 (aux l1)))
  21 ) in aux))
  22 ;;
  23
  24 let id_list =
  25 let rec id_list =
  26 (function l ->
  27 (match l with
  28    Nil -> (Nil)
  29  | Cons(hd,tl) -> (Cons(hd,(id_list tl))))
  30 ) in id_list
  31 ;;
  32
  33 let append =
  34 let rec append =
  35 (function l1 -> (function l2 ->
  36 (match l1 with
  37    Nil -> l2
  38  | Cons(hd,tl) -> (Cons(hd,(append tl l2))))
  39 )) in append
  40 ;;
  41
  42 let tail =
  43 (function l ->
  44 (match l with
  45    Nil -> (Nil)
  46  | Cons(hd,tl) -> tl)
  47 )
  48 ;;
  49
  50 let x1 =
  51 (Matita_nat_nat.S(Matita_nat_nat.O))
  52 ;;
  53
  54 let x2 =
  55 (Matita_nat_nat.S(x1))
  56 ;;
  57
  58 let x3 =
  59 (Matita_nat_nat.S(x2))
  60 ;;
  61
  62 let nth =
  63 let rec nth =
  64 (function l -> (function d -> (function n ->
  65 (match n with
  66    Matita_nat_nat.O ->
  67 (match l with
  68    Nil -> d
  69  | Cons(x,_) -> x)
  70
  71  | Matita_nat_nat.S(n') -> (nth (tail l) d n'))
  72 ))) in nth
  73 ;;
  74