Module dimensioned::peano [] [src]

Peano numbers allow us to do arithmetic at compile time using Rust's type system.

This module creates many traits. They are all used for arithmetic between Peano numbers and it is not recommended that you implement them for anything else.

Structs

Pred

For any number N that isn't a positive number, we define its predecessor. Mathematically, we have now defined all of the integers. We have actually defined -63 to 63.

Succ

For any number N, we define its successor. In mathematics, this and Zero are enough to get all the natural numbers; in Rust, it only gets us up to 63 as that is the most levels of embedded structs we can have.

Zero

The type-level number 0

Traits

AddPeano

This trait allows us to add any two Peano numbers.

DivPeano

This trait allows us to divide two Peano numbers so long as the numerator is divisible by the denominator.

KeepPeano

This trait does nothing, but it forces Self and RHS to be the same peano number.

MulPeano

This trait allows us to multiply any two Peano numbers.

Negate

This trait provides the negation of a number (e.g. -5 to 5)

NonNeg

All numbers of the form Succ<N> and Zero will belong to the trait NonNeg.

NonPos

All numbers of the form Pred<N> and Zero will belong to the trait NonNeg.

NonZero

All numbers of the form Succ<M> or Pred<N> will belong to the trait NonZero.

Peano

All numbers defined in this module will belong to the Peano trait.

SubPeano

This trait allows us to subtract any two Peano numbers.

ToInt

Converts a type to the integer it represents

Type Definitions

Eight
Five
Four
NegEight
NegFive
NegFour
NegNine
NegOne
NegSeven
NegSix
NegTen
NegThree
NegTwo
Nine
One
Seven
Six
Ten
Three
Two