more work on q

[helm.git] / helm / software / matita / library / list / list.ma

diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma
index f9f39bebf3b9dfde65c02733fbbb7955962deeaa..e4787fe8422fcf55a0888cc9da3b4d237239ff0c 100644 (file)
--- a/helm/software/matita/library/list/list.ma
+++ b/helm/software/matita/library/list/list.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/list/".
 include "logic/equality.ma".
 include "datatypes/bool.ma".
 include "higher_order_defs/functions.ma".
@@ -24,7 +23,7 @@ inductive list (A:Type) : Type :=
   | cons: A -> list A -> list A.
 
 notation "hvbox(hd break :: tl)"
-  right associative with precedence 46
+  right associative with precedence 47
   for @{'cons $hd $tl}.
 
 notation "[ list0 x sep ; ]"
@@ -42,8 +41,7 @@ interpretation "cons" 'cons hd tl =
 (* theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. *)
 
 theorem nil_cons:
-  \forall A:Type.\forall l:list A.\forall a:A.
-    a::l <> [].
+  \forall A:Type.\forall l:list A.\forall a:A. a::l ≠ [].
   intros;
   unfold Not;
   intros;
@@ -144,21 +142,29 @@ reflexivity.
 qed.
 *)
 
-let rec nth (A:Type) l d n on n ≝
- match n with
-  [ O ⇒
-     match l with
-      [ nil ⇒ d
-      | cons (x : A) _ ⇒ x
-      ]
-  | S n' ⇒ nth A (tail ? l) d n'
-  ].
+definition nth ≝
+  λA:Type.
+    let rec nth l d n on n ≝
+      match n with
+      [ O ⇒
+         match l with
+         [ nil ⇒ d
+         | cons (x : A) _ ⇒ x
+         ]
+      | S n' ⇒ nth (tail ? l) d n']
+    in nth.
   
-let rec map (A,B:Type) (f: A → B) (l : list A) on l : list B ≝
-  match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
+definition map ≝
+  λA,B:Type.λf:A→B.
+  let rec map (l : list A) on l : list B ≝
+    match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map tl)]
+  in map.
   
-let rec foldr (A,B:Type) (f : A → B → B) (b : B) (l : list A) on l : B := 
-  match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr ? ? f b l)].
+definition foldr ≝
+  λA,B:Type.λf:A→B→B.λb:B.
+  let rec foldr (l : list A) on l : B := 
+    match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr l)]
+  in foldr.
    
 definition length ≝ λT:Type.λl:list T.foldr T nat (λx,c.S c) O l.
 
@@ -194,4 +200,4 @@ intros;elim l
   |simplify;apply (bool_elim ? (p a));intro
      [simplify;apply le_S_S;assumption
      |simplify;apply le_S;assumption]]
-qed.
\ No newline at end of file
+qed.