Struct dimensioned::peano::Succ

pub struct Succ<N: NonNeg> {
    // some fields omitted
}

For any non-negative Peano number N, we define its successor, Succ<N>.

This gives us Peano numbers up to 63, as Rust only supports 64 levels of embedded structs.

Trait Implementations

impl<N: NonNeg> Peano for Succ<N>

impl<N: NonNeg> NonNeg for Succ<N>

impl<N: NonNeg> !NonPos for Succ<N>

impl<N: NonNeg> NonZero for Succ<N>

impl<Lhs, Rhs> Add<Rhs> for Succ<Lhs> where Lhs: NonNeg + Add<Rhs>, Rhs: NonNeg, Lhs::Output: NonNeg

Add non-negative numbers to positive numbers (e.g. 2 + 3, 2 + 0)

type Output = Succ<Lhs::Output>

fn add(self, rhs: Rhs) -> Self::Output

impl<Lhs, Rhs> Add<Pred<Rhs>> for Succ<Lhs> where Lhs: NonNeg + Add<Rhs>, Rhs: NonPos

Add negative and positive numbers (e.g. 2 + -3)

type Output = Lhs::Output

fn add(self, rhs: Pred<Rhs>) -> Self::Output

impl<N> Neg for Succ<N> where N: NonNeg + Neg, N::Output: NonPos

Negate positive numbers (e.g. 5 -> -5)

type Output = Pred<N::Output>

fn neg(self) -> Self::Output

impl<Lhs> Sub<Zero> for Succ<Lhs> where Lhs: NonNeg

Subtract Zero from positive numbers (e.g. 2 - 0)

type Output = Succ<Lhs>

fn sub(self, rhs: Zero) -> Self::Output

impl<Lhs, Rhs> Sub<Succ<Rhs>> for Succ<Lhs> where Lhs: NonNeg + Sub<Rhs>, Rhs: NonNeg

Subtract positive numbers from positive numbers (e.g. 3 - 4)

type Output = Lhs::Output

fn sub(self, rhs: Succ<Rhs>) -> Self::Output

impl<Lhs, Rhs> Sub<Pred<Rhs>> for Succ<Lhs> where Lhs: NonNeg + Sub<Rhs>, Rhs: NonPos, Lhs::Output: NonNeg

Subtract negative numbers from positive numbers (e.g. 3 - -4)

type Output = Succ<Succ<Lhs::Output>>

fn sub(self, rhs: Pred<Rhs>) -> Self::Output

impl<Lhs, Rhs> Mul<Rhs> for Succ<Lhs> where Lhs: NonNeg + Mul<Rhs>, Rhs: Add<Lhs::Output>

Multiply positive numbers by integers (e.g. 2 * N)

type Output = Rhs::Output

fn mul(self, rhs: Rhs) -> Self::Output

impl<Lhs, Rhs> Div<Rhs> for Succ<Lhs> where Lhs: NonNeg, Succ<Lhs>: DivPrivate<Rhs>

Divide a positive number by a non-zero number (e.g. 4 / 2, 4 / -2). Only defined for numbers that are evenly divisible.

type Output = Succ<Lhs>::Output

fn div(self, rhs: Rhs) -> Self::Output

impl<N: NonNeg + ToInt> ToInt for Succ<N>

fn to_int() -> i32

Derived Implementations

impl<N: Clone + NonNeg> Clone for Succ<N> where N: Clone

fn clone(&self) -> Succ<N>

fn clone_from(&mut self, source: &Self)

impl<N: Copy + NonNeg> Copy for Succ<N> where N: Copy