X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Flist.ma;h=d6c0661208c15e31c7b10684657a3f98bbd0060c;hb=b40e4e96e85103c7072985990c6b541371fd5a48;hp=39fdb1bd5ca9f550d6f3b1d37e72395af2c8546d;hpb=44ef2738ac6d7544c22950602eecf1eb61a80729;p=helm.git

diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma
index 39fdb1bd5..d6c066120 100644
--- a/weblib/basics/list.ma
+++ b/weblib/basics/list.ma
@@ -9,7 +9,7 @@
      \ /   GNU General Public License Version 2   
       V_______________________________________________________________ *)
 
-include "arithmetics/nat.ma".span class="error" title="disambiguation error"/span
+include "arithmetics/nat.ma".
 
 inductive list (A:Type[0]) : Type[0] :=
   | nil: list A
@@ -134,7 +134,7 @@ let rec rev_append S (l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"li
 
 definition reverse ≝λS.λl.a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"rev_append/a S l a title="nil" href="cic:/fakeuri.def(1)"[/a].
 
-lemma reverse_single : ∀S,a. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S a title="cons" href="cic:/fakeuri.def(1)"[/aa] a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="cons" href="cic:/fakeuri.def(1)"[/aa]. 
+lemma reverse_single : ∀S,a. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]). 
 // qed.
 
 lemma rev_append_def : ∀S,l1,l2. 
@@ -142,7 +142,7 @@ lemma rev_append_def : ∀S,l1,l2.
 #S #l1 elim l1 normalize // 
 qed.
 
-lemma reverse_cons : ∀S,a,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l)a title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aa].
+lemma reverse_cons : ∀S,a,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l)a title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]).
 #S #a #l whd in ⊢ (??%?); // 
 qed.
 
@@ -158,7 +158,7 @@ normalize // qed.
 (* an elimination principle for lists working on the tail;
 useful for strings *)
 lemma list_elim_left: ∀S.∀P:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S → Prop. P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a S) →
-(∀a.∀tl.P tl → P (tla title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aa])) → ∀l. P l.
+(∀a.∀tl.P tl → P (tla title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]))) → ∀l. P l.span class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"/span
 #S #P #Pnil #Pstep #l <(a href="cic:/matita/basics/list/reverse_reverse.def(9)"reverse_reverse/a … l) 
 generalize in match (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l); #l elim l //
 #a #tl #H >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a @Pstep //
@@ -237,4 +237,4 @@ theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/basics/list/list.ind(1,0,1
     a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈(Ia title="append" href="cic:/fakeuri.def(1)"@/aJ)} (f i).
 #A #B #I #J #nil #op #f (elim I) normalize 
   [>a href="cic:/matita/basics/list/nill.fix(0,2,2)"nill/a //|#a #tl #Hind <a href="cic:/matita/basics/list/assoc.fix(0,2,2)"assoc/a //]
-qed.
\ No newline at end of file
+qed.