Rel is a stateless relation on a discrete bounded chain T on which a law of Arity variables can be decided: a step (successor, by argument-dependent lookup, as for HasNNOStep), a least and a greatest value (the identities of Sup and Inf), the top reached from the bottom within chain_walk_budget, and nᴬʳⁱᵗʸ within law_evaluation_budget, all as constant expressions (what cannot be evaluated at compile time is simply not decided here, rather than an error). More...

Concept definition

template<typename T, typename Rel, std::size_t Arity>
concept dedekind::category::IsWalkableChain = 
    std::default_initializable<Rel> && std::is_empty_v<Rel> && requires {
      unit<T>(Sup{});
      unit<T>(Inf{});
    } && requires(const Rel& r, const T& x) {
      { r(x, x) } -> std::convertible_to<bool>;
      { successor(x) } -> std::convertible_to<T>;
      { x == x } -> std::convertible_to<bool>;
    } && requires {
      typename std::integral_constant<
          std::size_t, chain_length(unit<T>(Sup{}), unit<T>(Inf{}))>;
    } && fits_budget(chain_length(unit<T>(Sup{}), unit<T>(Inf{})), Arity)

Detailed Description

Rel is a stateless relation on a discrete bounded chain T on which a law of Arity variables can be decided: a step (successor, by argument-dependent lookup, as for HasNNOStep), a least and a greatest value (the identities of Sup and Inf), the top reached from the bottom within chain_walk_budget, and nᴬʳⁱᵗʸ within law_evaluation_budget, all as constant expressions (what cannot be evaluated at compile time is simply not decided here, rather than an error).

Note: The step must be the chain's cover, so the walk visits every value: that is what makes the chain discrete, the carrier's obligation, not checked here. Order: a carrier's step and bounds must be declared before anything asks about one of its relations (as for every trait registration: an answer, once instantiated, is fixed).