Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind::sets::detail_recursion_witness::FormsDescendingRecursion Concept Reference
module dedekind.sets

Concept definition

template<typename T>
concept dedekind::sets::detail_recursion_witness::FormsDescendingRecursion =
requires { 𝔸<T>{} & ((π == T{}) || χ(π - T{1})); }
dedekind::sets::detail_recursion_witness::FormsDescendingRecursion
Definition recursion.cppm:361
dedekind::category::π
constexpr Projection< 0 > π
The unary projection, the identity: the variable of a comprehension over one carrier.
Definition limit.cppm:350
dedekind::sets::𝔸
The universal set over the carrier T: the terminal object ⊤ of Sub(T), the reified type constraint.
Definition boundaries.cppm:296