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.

Subsections

• Creation of Coproducts
• Creation of Coproduct Elements

cop< [ S_1, S_2, ..., S_k ] > : [ Struct, Struct, ... ] -> Cop, [ Map ]

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

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.

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.