dedekind::sequences::detail_pst_witness Namespace Reference

Classes
struct	Run
	A maximal run of membership as its closed ends, [lo, hi]. More...

Functions
template<typename View>
consteval auto	summary (View v)
	A run list's runs as (count, first, last).
template<typename A>
constexpr Maybe< std::decay_t< A > >	η (A value)
	The Maybe endofunctor T, implemented via std::optional.

Variables
constexpr auto	above_bottom = 𝔸<Ternary>{} & (π > Ternary::False)
constexpr auto	above5 = 𝔸<int>{} & (π > 5)
constexpr auto	below3 = 𝔸<int>{} & (π < 3)
constexpr auto	hedge = 𝔸<Ternary, Kleene>{} & Identity<Ternary>{}
constexpr auto	cut_u
constexpr auto	fibre_u
constexpr Projection< 0 >	π
	The unary projection, the identity: the variable of a comprehension over one carrier.

Detailed Description

pst__Formal_Verification

Variable Documentation

cut_u

auto dedekind::sequences::detail_pst_witness::cut_u

inlineconstexpr

Initial value:

=
    𝔸<Ternary>{} & preimage(hedge, 𝔸<Ternary>{} & (π >= Ternary::Unknown))

fibre_u

auto dedekind::sequences::detail_pst_witness::fibre_u

inlineconstexpr

Initial value:

=
    𝔸<Ternary>{} & preimage(hedge, η(Ternary::Unknown))