Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind::sequences::HasPrefixBound Concept Reference
module dedekind.sequences

A relation is bounded (composable over a finite middle) iff its predicate carries a prefix_bound. More...

Concept definition

template<typename P>
concept dedekind::sequences::HasPrefixBound = requires(const P& p) {
{ prefix_bound(p) } -> std::convertible_to<std::size_t>;
}
dedekind::sequences::HasPrefixBound
A relation is bounded (composable over a finite middle) iff its predicate carries a prefix_bound.
Definition relprod.cppm:125
dedekind::sequences::prefix_bound
constexpr std::size_t prefix_bound(const dedekind::order::ProductRestrict< Pp, dedekind::sets::Cmp< dedekind::sets::Rel::Lt, dedekind::sets::Projection< 1 >, dedekind::sets::Const< K > > > &p)
prefix_bound(p) — recover the finite-prefix bound M carried by a bounded relation's predicate p: eith...
Definition relprod.cppm:110

Detailed Description

A relation is bounded (composable over a finite middle) iff its predicate carries a prefix_bound.