Module 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.


module L : CARDINAL
module R : CARDINAL


include CARDINAL
type n
val n : n cardinal
val inj_l : L.n index -> n index
val inj_r : R.n index -> n index
val prj : n index -> (L.n indexR.n index) either