Structural concept for a commutative semiring with total order (the intensional ℕ). More...

Concept definition

template<typename N>
concept dedekind::numbers::IsNatural =  dedekind::algebra::HasSemiringOperators<N> &&
                    dedekind::category::IsCommutativeMonoid<N, std::plus<N>> &&
                    dedekind::order::IsTotallyOrdered<N>

Detailed Description

Structural concept for a commutative semiring with total order (the intensional ℕ).

Deliberately not restricted to std::unsigned_integral<N> so that user-defined certified natural-number types (e.g. ExtensionalCardinal<>) can satisfy the concept without being built-in C++ types. The required operations are exactly those that characterise ℕ as a commutative semiring with a total order:

Additive monoid: +.
Multiplicative monoid: *.
Total order: <=.
No subtraction required — that is what distinguishes ℕ from ℤ.

Embedding from std::unsigned_integral: machine unsigned types are the extensional/IEEE-policy approximation of ℕ. Use embed_unsigned_integral<N>(v) to inject a machine value into a certified IsNatural domain, and realize_to_size_t(sentinel) to project back.

Wikipedia: Semiring, Peano axioms