X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Flist2.ma;h=5d9929fc0e89dd6c3424605e25ba4881eb3a34ad;hb=5431da8145e4a84596d312fc02b552881d119100;hp=1dd62c11459a888898d91cf32d0233ed0cf05ce4;hpb=8f08fac33a366b2267b35af1a50ad3a9df8dbb88;p=helm.git

diff --git a/weblib/basics/list2.ma b/weblib/basics/list2.ma
index 1dd62c114..5d9929fc0 100644
--- a/weblib/basics/list2.ma
+++ b/weblib/basics/list2.ma
@@ -15,16 +15,15 @@
 include "basics/list.ma".
 include "arithmetics/nat.ma".
 
-nlet rec length (A:Type) (l:list 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 ⇒ 0
-    | cons a tl ⇒ S (length A tl)].
+    [ 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)].
 
 notation "|M|" non associative with precedence 60 for @{'norm $M}.
 interpretation "norm" 'norm l = (length ? l).
 
-nlet rec nth n (A:Type) (l:list 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 ⇒ hd A l d
-    |S m ⇒ nth m A (tail A l) d].
-
+    [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].
\ No newline at end of file