| | 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) |
|
| eq_int | Def i= j == if i=j true ; false fi |
| | | Thm* i,j: . (i=j) |
|
| 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 |
|
| nat | Def == {i:| 0i } |
| | | Thm* Type |
