dedekind::numbers::Interval< V, L > Struct Template Reference

A convex subset of a chain as a VALUE — an interval: each side an optional Bound, with a runtime-evaluable membership χ. Closed under ∩; a union or a complement leaves it unless one operand covers the other. No side is the universe; both sides closed at one value is a point; no Span at all is the one empty set, to which crossing bounds normalise. The bounds ride as values, never as NTTPs. Consume it through &, |, ==, <=, membership and the half / point / empty / universe / bounded factories. More...

Inheritance diagram for dedekind::numbers::Interval< V, L >:

Collaboration diagram for dedekind::numbers::Interval< V, L >:

Public Types
using	Domain = V
using	Codomain = typename L::Ω
using	cardinality_type = carrier_cardinality_t<V>
Public Types inherited from dedekind::sets::SetExpr< Interval< V, Boole >, V, Boole >
using	Domain
using	Codomain
using	logic_species

Public Member Functions
constexpr	Interval ()=default
	The universe, 𝔸.
constexpr const std::optional< Span< V > > &	span () const
	The sides, or nullopt for Ø: a convex set is 1 + Span. Built only through the factories below, so always in normal form.
constexpr bool	contains (const V &x) const
	χ(x): runtime membership, decided from the value fields.
constexpr bool	contains_bounded (const V &x) const
	The sides' comparisons against the carrier.
constexpr L::Ω	operator() (const V &x) const
	ETCS χ: contains lifted to the logic species L.
Public Member Functions inherited from dedekind::sets::SetExpr< Interval< V, Boole >, V, Boole >
constexpr V	ι (const Member &m) const

Static Public Member Functions
static constexpr Interval	half (V pivot, Direction d, Strictness s)
	The ray {x ⋈ pivot}. Whether it is empty, or all of the carrier, at the carrier's end is read by == Ø / == 𝔸.
static constexpr Interval	point (V pivot)
static constexpr Interval	empty ()
	The two boundary sets as values — the meet's annihilator (Ø) and unit (𝔸). Factories (not raw aggregate init) so callers never spell the empty-base brace of the SetExpr aggregate.
static constexpr Interval	universe ()
static constexpr Interval	bounded (V lo, Strictness sl, V hi, Strictness su)
	The bounded meet [lo, hi] with its strictness pair, collapsed: empty if the bounds cross, the single point where the chain admits exactly one element, else the interval. The ONE collapse law every meet rides. The point collapse gates on the NNO steps (HasNNOStep: successor / predecessor, an axiom of the category), so the ℕ proxy Cardinality collapses to its point exactly as a machine integer does.
static constexpr Interval	of_sides (const std::optional< Bound< V > > &lo, const std::optional< Bound< V > > &hi)
	The set with the given sides: through bounded when both are present, so it is collapsed.

Detailed Description

template<typename V, typename L = Boole>
requires IsTotallyOrdered<V> && IsOckhamAlgebra<L>
struct dedekind::numbers::Interval< V, L >

A convex subset of a chain as a VALUE — an interval: each side an optional Bound, with a runtime-evaluable membership χ. Closed under ∩; a union or a complement leaves it unless one operand covers the other. No side is the universe; both sides closed at one value is a point; no Span at all is the one empty set, to which crossing bounds normalise. The bounds ride as values, never as NTTPs. Consume it through &, |, ==, <=, membership and the half / point / empty / universe / bounded factories.

The carrier is gated on the registered chain (IsTotallyOrdered): a cut is a normal form only on a chain.

Template Parameters

V	the carrier.
L	the species.

Member Function Documentation

contains()

template<typename V, typename L = Boole>

bool dedekind::order::Interval< V, L >::contains ( const V & x ) const

inlineconstexpr

χ(x): runtime membership, decided from the value fields.

The two DECIDED cases (⊥ / ⊤) need no carrier comparison, so they are answered in this small front and the carrier comparisons live in contains_bounded behind it. The split is load-bearing for the IR exhibits: on a variant carrier (ℕ = Cardinality) the comparisons are heavy enough that the inliner declines a single fat function, and a constant Interval then stays a call instead of folding to ret i1 false. A small front inlines, the loads from the constant fold, and the bounded call is dead code.

of_sides()

template<typename V, typename L = Boole>

constexpr Interval dedekind::order::Interval< V, L >::of_sides ( const std::optional< Bound< V > > & lo, const std::optional< Bound< V > > & hi )

inlinestaticconstexpr

The set with the given sides: through bounded when both are present, so it is collapsed.

Parameters

lo	the lower side.
hi	the upper side.

---

The documentation for this struct was generated from the following file:

• src/main/modules/dedekind/order/halfspace.cppm