- Generated by
1.15.0
|
Dedekind 0.0.0
A structuralist C++23 Module Library
|
The projection π_k: the k-th component of a product.
More...
Public Member Functions | |
|
template<typename P> requires requires(const P& p) { component(p, At<K>{}); } | |
| constexpr auto | operator() (const P &p) const |
| The component, as a value: one overload for lvalues and temporaries alike, and no reference into a product that may die. | |
The projection π_k: the k-th component of a product.
The variables of the grammar are the product projections of category:limit, one entity each: π (the unary projection, the identity), π_1, π_2, π_3, and the family π_<k>.
| K | the slot, from 1. |
π leaves the carrier open: π > 5 is a cut datum, π == v a point, and the former carrier & ... binds it, the constant meeting the carrier exactly. On a product the variable of slot k is the projection π_k: called on a point it reads the coordinate, and a comparison of terms over it builds a strongly-typed predicate on the pair (no lambda); && conjoins them (|| joins), distinct from the set-level & / | on whole relations; and product | predicate restricts the product to the relation. && binds looser than |, so the comprehension parenthesises the meet: ℕ*ℕ & (π_1 < π_2 && π_1 > 5) is the relation \(\{(x,y) \mid x<y \wedge x>5\}\) as an IsSet on ℕ×ℕ.
1.15.0