`Indexing.Sum`

`Sum(L)(R)`

creates a new type-level set, which is the disjoint sums of the sets `L`

and `R`

. The functor application `Sum(L)(R)`

involves a call to `cardinal L.n`

, thereby fixing the cardinal of the set `L`

, if it was an open-ended set. The cardinal of the set `R`

is not fixed: if `R`

is an open-ended set, then the new set is open-ended as well, and it is still permitted to add new elements to `R`

by calling `R.fresh()`

. Fixing the cardinal of the new set fixes the cardinal of `R`

.