X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Flist2.ma;h=5d9929fc0e89dd6c3424605e25ba4881eb3a34ad;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=2543b3084a52c09fae87853bc54fb96f6c36a446;hpb=b8a719bbb47d12e0a6b2c8cb2e5e26a2bf360be1;p=helm.git

diff --git a/weblib/basics/list2.ma b/weblib/basics/list2.ma
index 2543b3084..5d9929fc0 100644
--- a/weblib/basics/list2.ma
+++ b/weblib/basics/list2.ma
@@ -15,7 +15,7 @@
 include "basics/list.ma".
 include "arithmetics/nat.ma".
 
-let rec length (A:Type[0]) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝ 
+img class="anchor" src="icons/tick.png" id="length"let rec length (A:Type[0]) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝ 
   match l with 
     [ nil ⇒ a title="natural number" href="cic:/fakeuri.def(1)"0/a
     | cons a tl ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (length A tl)].
@@ -23,7 +23,7 @@ let rec length (A:Type[0]) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"
 notation "|M|" non associative with precedence 60 for @{'norm $M}.
 interpretation "norm" 'norm l = (length ? l).
 
-let rec nth n (A:Type[0]) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (d:A)  ≝  
+img class="anchor" src="icons/tick.png" id="nth"let rec nth n (A:Type[0]) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (d:A)  ≝  
   match n with
     [O ⇒ a href="cic:/matita/basics/list/hd.def(1)"hd/a A l d
-    |S m ⇒ nth m A (a href="cic:/matita/basics/list/tail.def(1)"tail/a A l) d].
+    |S m ⇒ nth m A (a href="cic:/matita/basics/list/tail.def(1)"tail/a A l) d].
\ No newline at end of file