| Some definitions of interest. |
|
int_seg | Def {i..j} == {k:| i k < j } |
| | Thm* m,n:. {m..n} Type |
|
nat | Def == {i:| 0i } |
| | Thm* Type |
|
le | Def AB == B<A |
| | Thm* i,j:. (ij) Prop |
|
listify | Def f{m..n} == if nm nil else f(m).f{(m+1)..n} fi (recursive) |
| | Thm* T:Type, m,n:, f:({m..n}T). f{m..n} T List |
|
le_int | Def ij == j<i |
| | Thm* i,j:. (ij) |