Creation Functions

There are two versions of the coproduct constructor. Ordinarily, coproducts will be constructed from a list of structures. These structures are called the constituents of the coproduct. A single sequence argument is allowed as well to be able to create coproducts of parameterized families of structures conveniently.

Creation of Coproducts

cop< S₁, S₂, ..., S_k > : Str, Str, ... -> Cop, [ Map ]

cop< [ S₁, S₂, ..., S_k ] > : [ Str, Str, ... ] -> Cop, [ Map ]

Given a list or a sequence of two or more structures S₁, S₂, ..., S_k, this function creates and returns their coproduct C as well as a sequence of maps [m₁, m₂, ..., m_k] that provide the injections m_i: S_i -> C.

Creation of Coproduct Elements

Coproduct elements are usually created by the injections returned as the second return value from the cop<> constructor. The bang (!) operator may also be used but only if the type of the relevant constituent is unique for the particular coproduct.

m(e) : Map, Elt -> CopElt

Given a coproduct injection map m and an element of one of the constituents of the coproduct C, create the coproduct element version of e.

C ! e : Cop, Elt -> CopElt

Given a coproduct C and an element e of one of the constituents of C such that the type of that constituent is unique within that coproduct, create the coproduct element version of e.