dedekind::sets::detail_recursion_witness Namespace Reference

Concepts
concept	FormsNonDescendingRecursion
concept	FormsDescendingRecursion
concept	FormsSamePointRecursion
concept	FormsCyclingRecursion
concept	FormsMeasuredRecursion

Typedefs
using	N = std::size_t
using	NN = std::pair<N, N>
using	FiniteN = 𝔸<unsigned, dedekind::category::Boole, Finite>

Variables
constexpr auto	multiples_of_3 = 𝔸<N>{} & ((π == N{0}) || χ(π - N{3}))
constexpr auto	naturals = 𝔸<N>{} & ((π == N{0}) || χ(π - N{1}))
constexpr auto	y_zero_or_x_positive
constexpr auto	finite_evens = FiniteN{} & ((π == 0u) || χ(π - 2u))

Detailed Description

recursion__Formal_Verification

Variable Documentation

y_zero_or_x_positive

auto dedekind::sets::detail_recursion_witness::y_zero_or_x_positive

inlineconstexpr

Initial value:

=
    𝔸<NN>{} & ((π_2 == N{0}) || χ(π_1 - N{1}, N{0}))