| Some definitions of interest. |
|
eval_factorization | Def {a..b}(f) == i:{a..b}. if(i) |
| | Thm* a,b:, f:({a..b}). {a..b}(f) |
|
int_seg | Def {i..j} == {k:| i k < j } |
| | Thm* m,n:. {m..n} Type |
|
int_upper | Def {i...} == {j:| ij } |
| | Thm* n:. {n...} Type |
|
nat | Def == {i:| 0i } |
| | Thm* Type |