sets.cppm

Go to the documentation of this file.

export module dedekind.sets;
 
export import :cardinality;
export import :boundaries;
export import :computability;
export import :terms;  // the term grammar: projections, constants, atoms
export import :expressions;
export import :heterogeneous;  // across carriers: A × B, A + B, the ℕ / ℤ
                               // widening
export import :extensional;
export import :quantifier;
export import :singleton;
export import :recursion;  // χ: inductive sets, the former closing a structural
                           // recursion
// :relational (Codd's σ ⋈ ∪ ∖) and :graph (graphs of arrows) were popped OUT of
// :sets into the dedekind.relational module (above sets, below order; GH #792).