|
|
constexpr T | ι (const Member &m) const |
| | ι: Ø ↣ T — the trivial inclusion. No members are ever constructed, so ι is unreachable in practice; the body unwraps the Member's T-value to satisfy the SHAPE the IsSubobject contract reads.
|
template<typename OtherL>
requires (!std::same_as<OtherL, L>) |
| constexpr | Ø (const Ø< T, OtherL > &) |
| | Cross-logic identity: the empty set under any logic species is the empty set. Enables writing Ø<int> (L defaults to Boole) even when the RHS answers in Kleene — mathematically ∅ = ∅ regardless of logic species.
|
| constexpr std::size_t | size () const |
| template<typename S> |
| constexpr L::Ω | operator<= (const S &) const |
|
constexpr bool | operator== (const Ø &) const |
template<typename T2, typename L2>
requires (!std::same_as<T, T2> || !std::same_as<L, L2>) |
| constexpr bool | operator== (const Ø< T2, L2 > &) const |
template<typename S>
requires (IsLSet<S> || std::ranges::range<S>) && (!std::same_as<S, Ø>) && requires(const S& s) { { s.size() } -> std::convertible_to<std::size_t>; } |
| constexpr bool | operator== (const S &s) const |
|
constexpr auto | operator! () const |
|
constexpr L::Ω | operator() (const T &) const |
|
constexpr cardinality_type | cardinality () const |
|
constexpr std::size_t | upper_bound () const |
template<typename S>
requires (IsLSet<S>) |
| constexpr auto | operator^ (const S &s) const |
template<typename S>
requires (IsLSet<S>) |
| constexpr auto | operator* (const S &) const |
| | Ø × S = Ø<pair<T, S::Domain>, Boole>. Empty annihilates the cartesian product on the left. Carrier widens to the pair type; the codomain is Boolean (an empty product is decided, #894).
|
template<typename T = std::nullptr_t, typename L = Boole>
struct dedekind::sets::Ø< T, L >
∅: The Initial Object. Extensional (Size 0).
T defaults to std::nullptr_t (the project's Zero carrier), so the bare Ø{} denotes "the empty set" with no carrier to name; it compares equal to any Ø<T> through the cross-carrier operator== below, letting a collapse be asserted as (a & ~a) == Ø{}.