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.

Parameters

module L : CARDINAL

module R : CARDINAL

Signature

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 index, R.n index) either