| | Some definitions of interest. |
|
| sized_bool | Def  a {k}  == {p:(a  )| size(a)(p) = k } |
| | | Thm*  a,k:. a {k}  Type |
|
| boolsize | Def size(a)(p) == Msize( x.if p(x) 1 else 0 fi) |
| | | Thm* a:. size(a) (a) |
|
| sized_mset | Def a {k} T == {p:(aT)| Msize(p) = k } |
| | | Thm* a,k:. a {k} Type |
| | | Thm* a,k,x:, y: . a {k} {x..y } Type |
| | | Thm* a,k,x:, y:. a {k} {x...y} Type |
| | | Thm* a,k:. a {k}  Type |
| | | Thm* a,k,x:. a {k} {x...} Type |
|
| int_seg | Def {i..j} == {k:| i  k < j } |
| | | Thm* m,n:. {m..n} Type |
|
| msize | Def Msize(f) ==  i:k. f(i) |
| | | Thm* k:. Msize (k) |
|
| nat | Def == {i:| 0i } |
| | | Thm* Type |
