manual commit after active hyperlinks

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

diff --git a/weblib/basics/list2.ma b/weblib/basics/list2.ma
index 2543b3084a52c09fae87853bc54fb96f6c36a446..5d9929fc0e89dd6c3424605e25ba4881eb3a34ad 100644 (file)
--- 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:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 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 ⇒ \ 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)].
@@ -23,7 +23,7 @@ let rec length (A:Type[0]) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6
 notation "|M|" non associative with precedence 60 for @{'norm $M}.
 interpretation "norm" 'norm l = (length ? l).
 
-let 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)  ≝  
+\ 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 ⇒ \ 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].
+    |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