| Some definitions of interest. |
|
listify | Def f{m..n } == if n![](FONT/le.png) m nil else f(m).f{(m+1)..n } fi (recursive) |
| | Thm* T:Type, m,n: , f:({m..n }![](FONT/dash.png) T). f{m..n } T List |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
|
select | Def l[i] == hd(nth_tl(i;l)) |
| | Thm* A:Type, l:A List, n: . 0 n ![](FONT/eq.png) n<||l|| ![](FONT/eq.png) l[n] A |