Update online helper entries

[helm.git] / weblib / basics / list2.ma

diff --git a/weblib/basics/list2.ma b/weblib/basics/list2.ma
index 1dd62c11459a888898d91cf32d0233ed0cf05ce4..5d9929fc0e89dd6c3424605e25ba4881eb3a34ad 100644 (file)
--- 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 ≝ 
+\ 5img class="anchor" src="icons/tick.png" id="length"\ 6let rec length (A:Type[0]) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝ 
   match l with 
-    [ nil ⇒ 0
-    | cons a tl ⇒ S (length A tl)].
+    [ nil ⇒ \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6
+    | cons a tl ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (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)  ≝  
+\ 5img class="anchor" src="icons/tick.png" id="nth"\ 6let rec nth n (A:Type[0]) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (d:A)  ≝  
   match n with
-    [O ⇒ hd A l d
-    |S m ⇒ nth m A (tail A l) d].
-
+    [O ⇒ \ 5a href="cic:/matita/basics/list/hd.def(1)"\ 6hd\ 5/a\ 6 A l d
+    |S m ⇒ nth m A (\ 5a href="cic:/matita/basics/list/tail.def(1)"\ 6tail\ 5/a\ 6 A l) d].
\ No newline at end of file