| Some definitions of interest. |
|
flip | Def (i, j)(x) == if x= i j ; x= j i else x fi |
| | Thm* k: , i,j: k. (i, j) k  k |
|
int_seg | Def {i..j } == {k: | i k < j } |
| | Thm* m,n: . {m..n } Type |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
|
sum | Def sum(f(x) | x < k) == primrec(k;0; x,n. n+f(x)) |
| | Thm* n: , f:( n  ). sum(f(x) | x < n)  |