Trait type_level_logic::strong::ternary::NatPred

pub trait NatPred: Nat {
    type Output: Nat;
}

The Pred operator subtracts one from a Nat. It is defined for non-zero Nats, and can be used as Pred<X> or <X as NatPred>::Output.

Associated Types

type Output: Nat

Implementors

• impl NatPred for Undefined
• impl NatPred for Term
• impl<X: Nat> NatPred for Zero<X> where
    X: NatPred, 
• impl<X: Nat> NatPred for One<X> where
    X: NatTriple, 
• impl<X: Nat> NatPred for Two<X>