Trait NatAdd

pub trait NatAdd<B: Nat>: Nat {
    type Output: Nat;
}

Nat addition. Used as Add<X, Y> or <X as NatAdd<Y>>::Output.

Required Associated Types

type Output: Nat

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl NatAdd<Term> for Term

type Output = Term

impl NatAdd<Term> for Undefined

type Output = Undefined

impl NatAdd<Undefined> for Term

type Output = Undefined

impl NatAdd<Undefined> for Undefined

type Output = Undefined

impl<X> NatAdd<Term> for Zero<X>

where X: NatTriple + Nat,

type Output = <X as NatTriple>::Output

impl<X> NatAdd<Zero<X>> for Term

where X: NatTriple + Nat,

type Output = <X as NatTriple>::Output

impl<X, Y: Nat> NatAdd<One<Y>> for One<X>

where X: NatAdd<Y> + Nat,

type Output = Two<<X as NatAdd<Y>>::Output>

impl<X, Y: Nat> NatAdd<One<Y>> for Two<X>

where <X as NatAdd<Y>>::Output: NatSucc, X: NatAdd<Y> + Nat,

type Output = Zero<<<X as NatAdd<Y>>::Output as NatSucc>::Output>

impl<X, Y: Nat> NatAdd<One<Y>> for Zero<X>

where X: NatAdd<Y> + Nat,

type Output = One<<X as NatAdd<Y>>::Output>

impl<X, Y: Nat> NatAdd<Two<Y>> for One<X>

where <X as NatAdd<Y>>::Output: NatSucc, X: NatAdd<Y> + Nat,

type Output = Zero<<<X as NatAdd<Y>>::Output as NatSucc>::Output>

impl<X, Y: Nat> NatAdd<Two<Y>> for Two<X>

where <X as NatAdd<Y>>::Output: NatSucc, X: NatAdd<Y> + Nat,

type Output = One<<<X as NatAdd<Y>>::Output as NatSucc>::Output>

impl<X, Y: Nat> NatAdd<Two<Y>> for Zero<X>

where X: NatAdd<Y> + Nat,

type Output = Two<<X as NatAdd<Y>>::Output>

impl<X, Y: Nat> NatAdd<Zero<Y>> for One<X>

where X: NatAdd<Y> + Nat,

type Output = One<<X as NatAdd<Y>>::Output>

impl<X, Y: Nat> NatAdd<Zero<Y>> for Two<X>

where X: NatAdd<Y> + Nat,

type Output = Two<<X as NatAdd<Y>>::Output>

impl<X, Y: Nat> NatAdd<Zero<Y>> for Zero<X>

where <X as NatAdd<Y>>::Output: NatTriple, X: NatAdd<Y> + Nat,

type Output = <<X as NatAdd<Y>>::Output as NatTriple>::Output

impl<X: Nat> NatAdd<One<X>> for Term

type Output = One<X>

impl<X: Nat> NatAdd<One<X>> for Undefined

type Output = Undefined

impl<X: Nat> NatAdd<Term> for One<X>

type Output = One<X>

impl<X: Nat> NatAdd<Term> for Two<X>

type Output = Two<X>

impl<X: Nat> NatAdd<Two<X>> for Term

type Output = Two<X>

impl<X: Nat> NatAdd<Two<X>> for Undefined

type Output = Undefined

impl<X: Nat> NatAdd<Undefined> for One<X>

type Output = Undefined

impl<X: Nat> NatAdd<Undefined> for Two<X>

type Output = Undefined

impl<X: Nat> NatAdd<Undefined> for Zero<X>

type Output = Undefined

impl<X: Nat> NatAdd<Zero<X>> for Undefined

type Output = Undefined