| Some definitions of interest. |
|
select | Def l[i] == hd(nth_tl(i;l)) |
| | Thm* A:Type, l:A List, n:. 0n n<||l|| l[n] A |
|
hd | Def hd(l) == Case of l; nil "?" ; h.t h |
| | Thm* A:Type, l:A List. ||l||1 hd(l) A |
|
le | Def AB == B<A |
| | Thm* i,j:. (ij) Prop |
|
length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| | Thm* A:Type, l:A List. ||l|| |
| | Thm* ||nil|| |
|
nth_tl | Def nth_tl(n;as) == if n0 as else nth_tl(n-1;tl(as)) fi (recursive) |
| | Thm* A:Type, as:A List, i:. nth_tl(i;as) A List |