dedekind::category::Predecessor< N > Struct Template Reference

The predecessor \(P : N \to N\) as an arrow, in the carrier's own posture at ⊥: the monus on ℕ (0 a fixpoint), −1 on ℤ. More...

Public Types
using	Domain = N
using	Codomain = N

Public Member Functions
constexpr N	operator() (const N &n) const noexcept(noexcept(predecessor(n)))

Detailed Description

template<HasNNOStep N>
struct dedekind::category::Predecessor< N >

The predecessor \(P : N \to N\) as an arrow, in the carrier's own posture at ⊥: the monus on ℕ (0 a fixpoint), −1 on ℤ.

Template Parameters

N	the carrier, with successor / predecessor.

Member Function Documentation

operator()()

template<HasNNOStep N>

N dedekind::category::Predecessor< N >::operator() ( const N & n ) const

inlineconstexprnoexcept

Parameters

n	an element of the carrier.

Returns

its predecessor, by the carrier's own predecessor; nothrow when that is.

---

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

• src/main/modules/dedekind/category/nno.cppm