| Some definitions of interest. |
|
double_sum | Def sum(f(x;y) | x < n; y < m) == sum(sum(f(x;y) | y < m) | x < n) |
| | Thm* n,m: , f:( n  m  ). sum(f(x,y) | x < n; y < m)  |
|
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)  |