Trait type_level_logic::strong::ternary::NatAdd

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

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

Associated Types

type Output: Nat

Implementors

• impl NatAdd<Term> for Term
• impl NatAdd<Term> for Undefined
• impl NatAdd<Undefined> for Term
• impl NatAdd<Undefined> for Undefined
• impl<X: Nat> NatAdd<Zero<X>> for Term where
    X: NatTriple, 
• impl<X: Nat> NatAdd<One<X>> for Term
• impl<X: Nat> NatAdd<Two<X>> for Term
• impl<X: Nat> NatAdd<Term> for Zero<X> where
    X: NatTriple, 
• impl<X: Nat> NatAdd<Term> for One<X>
• impl<X: Nat> NatAdd<Term> for Two<X>
• impl<X: Nat> NatAdd<Zero<X>> for Undefined
• impl<X: Nat> NatAdd<One<X>> for Undefined
• impl<X: Nat> NatAdd<Two<X>> for Undefined
• impl<X: Nat> NatAdd<Undefined> for Zero<X>
• impl<X: Nat> NatAdd<Undefined> for One<X>
• impl<X: Nat> NatAdd<Undefined> for Two<X>
• impl<X: Nat, Y: Nat> NatAdd<Zero<Y>> for Zero<X> where
    <X as NatAdd<Y>>::Output: NatTriple,
    X: NatAdd<Y>, 
• impl<X: Nat, Y: Nat> NatAdd<One<Y>> for Zero<X> where
    X: NatAdd<Y>, 
• impl<X: Nat, Y: Nat> NatAdd<Two<Y>> for Zero<X> where
    X: NatAdd<Y>, 
• impl<X: Nat, Y: Nat> NatAdd<Zero<Y>> for One<X> where
    X: NatAdd<Y>, 
• impl<X: Nat, Y: Nat> NatAdd<One<Y>> for One<X> where
    X: NatAdd<Y>, 
• impl<X: Nat, Y: Nat> NatAdd<Two<Y>> for One<X> where
    <X as NatAdd<Y>>::Output: NatSucc,
    X: NatAdd<Y>, 
• impl<X: Nat, Y: Nat> NatAdd<Zero<Y>> for Two<X> where
    X: NatAdd<Y>, 
• impl<X: Nat, Y: Nat> NatAdd<One<Y>> for Two<X> where
    <X as NatAdd<Y>>::Output: NatSucc,
    X: NatAdd<Y>, 
• impl<X: Nat, Y: Nat> NatAdd<Two<Y>> for Two<X> where
    <X as NatAdd<Y>>::Output: NatSucc,
    X: NatAdd<Y>,