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