a {k}
T == {p:(a
T)| Msize(p) = k }
a,k:. a {k} 
Typea,k,x:, y:
. a {k} {x..y
} Typea,k,x:, y:. a {k} {x...y} Typea,k:. a {k} 
Typea,k,x:. a {k} {x...} Type == {i:| 0
i } Type == {i:| 0<i } Type| Some definitions of interest. | |
| sized_mset | a {k} T == {p:(aT)| Msize(p) = k } |
| a,k:. a {k} Type | |
| a,k,x:, y:. a {k} {x..y} Type | |
| a,k,x:, y:. a {k} {x...y} Type | |
| a,k:. a {k} Type | |
| a,k,x:. a {k} {x...} Type | |
| nat | == {i:| 0i } |
| Type | |
| nat_plus | == {i:| 0<i } |
| Type |
About:
 |  |  |  |  |  |
 |  |  |  |  |