| Some definitions of interest. | |
| adjl_out | Def t.out == 2of(t) |
Thm*  t:AdjList. t.out   t.size  (t.size List) | |
| adjl_size | Def t.size == 1of(t) |
| Thm* t:AdjList. t.size | |
| adjlist | Def AdjList == size: size(size List) |
| Thm* AdjList Type | |
| int_seg | Def {i..j } == {k: | i  k < j } |
| Thm* m,n:. {m..n} Type | |
| length | Def ||as|| == Case of as; nil  0 ; a.as' ||as'||+1 (recursive) |
| Thm* A:Type, l:A List. ||l|| | |
| Thm* ||nil|| | |
| nat | Def == {i:| 0i } |
| Thm* Type | |
| select | Def l[i] == hd(nth_tl(i;l)) |
Thm* A:Type, l:A List, n:. 0n   n < ||l|| l[n] A |
About:
 |  |  |  |
 |  |  |  |  |  |
 |  |  |  |  |
 |