dedekind::sets::IsWhereClause Concept Reference

Quantifiers over a finite carrier, decided by type through the finite quotient rather than by enumeration. More...

Concept definition

template<typename P, typename S>
concept dedekind::sets::IsWhereClause =  !dedekind::category::IsLSet<std::remove_cvref_t<P>> &&
                        requires(const S& s, P p) { s & p; }

Detailed Description

Quantifiers over a finite carrier, decided by type through the finite quotient rather than by enumeration.

quantifier__Finite_Quotient

The comprehension is the meet S & P: on \(\mathbb{B}\) a fragment collapses structurally (π==v to a Singleton, π⋈v to a Halfspace), each carrying a finite ==Ø / ==𝔸 over {false, true}; on \(\mathbb{N}\) a congruence πn==r materialises to a ResidueClass, decided analytically. No range, no begin/end walk. See the §3.1 exhibit.

A where-clause over the set S: a fragment P for which S & P is the comprehension \(\{x \in S \mid P(x)\}\) — a datum (π == v, π > v) or a carrier-agnostic fragment (π == c, π % n == r), which has no domain until the former binds it. Not a set: S & T would be the meet of two sets. What the former returns is the fragment's business (a comprehension, a residue set), so only its acceptance is asked.

Template Parameters

P	the fragment.
S	the set it refines.