Provides a companion object for the sealed trait Nat, incorporating utility methods and type class instances for handling natural numbers defined via Peano arithmetic.
The object includes an implicit implementation of the Semiring type class, which introduces algebraic operations such as addition and multiplication specifically tailored for natural numbers (Nat).
Attributes
Members list
Type members
Classlikes
Provides an implementation of the Semiring type class for natural numbers (Nat), enabling operations such as addition and multiplication following the rules of Peano arithmetic.
Provides an implementation of the Semiring type class for natural numbers (Nat), enabling operations such as addition and multiplication following the rules of Peano arithmetic.
This instance defines the behavior for:
zero: The base natural numberNatZero, representing the additive identity.one: The smallest positive natural number, represented as the successor ofNatZero.plus: Addition of two natural numbers, defined recursively.times: Multiplication of two natural numbers, defined recursively using addition.compare: Comparison of two natural numbers, defined recursively.
Attributes
- Supertypes
-
trait Ordering[Nat]trait PartialOrdering[Nat]trait Equiv[Nat]trait Comparator[Nat]trait Semiring[Nat]trait MultiplicativeSemigroup[Nat]trait AdditiveCommutativeMonoid[Nat]trait AdditiveCommutativeSemigroup[Nat]trait AdditiveMonoid[Nat]trait AdditiveSemigroup[Nat]trait Serializableclass Objecttrait Matchableclass AnyShow all
- Self type
-
natIsSemiring.type
Inherited and Abstract types
The names of the product elements.
The names of the product elements.
Attributes
- Inherited from:
- Mirror
The name of the type.
The name of the type.
Attributes
- Inherited from:
- Mirror
Value members
Concrete methods
Converts a given non-negative integer into its corresponding Nat representation.
Converts a given non-negative integer into its corresponding Nat representation.
The method uses Peano arithmetic to construct the natural number representation. It begins with the base case NatZero and iteratively applies Succ to build the representation of the integer.
Value parameters
- x
-
A non-negative integer to be converted into a
Natrepresentation. Must be greater than or equal to 0.
Attributes
- Returns
-
The
Natrepresentation of the given integer. The result isNatZeroifxis 0, or aSuccchain equivalent toxifxis greater than 0.