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