Trait type_level_logic::strong::ternary::NatRem

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

Nat remainder. Used as Rem<X, Y> or <X as NatRem<Y>>::Output. Returns Undefined in the case of a division by zero.

Associated Types

type Output: Nat

Implementors

• impl NatRem<Term> for Term
• impl NatRem<Undefined> for Term
• impl NatRem<Term> for Undefined
• impl NatRem<Undefined> for Undefined
• impl<D: Nat> NatRem<Zero<D>> for Term
• impl<D: Nat> NatRem<One<D>> for Term
• impl<D: Nat> NatRem<Two<D>> for Term
• impl<N: Nat, D: Nat> NatRem<Zero<D>> for Zero<N> where
    <<Zero<N> as NatRev>::Output as NatDivInternal<Zero<D>, Nat2<Term, Term>>>::Output: Nat2P1,
    <Zero<N> as NatRev>::Output: NatDivInternal<Zero<D>, Nat2<Term, Term>>,
    Zero<N>: NatRev, 
• impl<N: Nat, D: Nat> NatRem<One<D>> for Zero<N> where
    <<Zero<N> as NatRev>::Output as NatDivInternal<One<D>, Nat2<Term, Term>>>::Output: Nat2P1,
    <Zero<N> as NatRev>::Output: NatDivInternal<One<D>, Nat2<Term, Term>>,
    Zero<N>: NatRev, 
• impl<N: Nat, D: Nat> NatRem<Two<D>> for Zero<N> where
    <<Zero<N> as NatRev>::Output as NatDivInternal<Two<D>, Nat2<Term, Term>>>::Output: Nat2P1,
    <Zero<N> as NatRev>::Output: NatDivInternal<Two<D>, Nat2<Term, Term>>,
    Zero<N>: NatRev, 
• impl<N: Nat, D: Nat> NatRem<Zero<D>> for One<N> where
    <<One<N> as NatRev>::Output as NatDivInternal<Zero<D>, Nat2<Term, Term>>>::Output: Nat2P1,
    <One<N> as NatRev>::Output: NatDivInternal<Zero<D>, Nat2<Term, Term>>,
    One<N>: NatRev, 
• impl<N: Nat, D: Nat> NatRem<One<D>> for One<N> where
    <<One<N> as NatRev>::Output as NatDivInternal<One<D>, Nat2<Term, Term>>>::Output: Nat2P1,
    <One<N> as NatRev>::Output: NatDivInternal<One<D>, Nat2<Term, Term>>,
    One<N>: NatRev, 
• impl<N: Nat, D: Nat> NatRem<Two<D>> for One<N> where
    <<One<N> as NatRev>::Output as NatDivInternal<Two<D>, Nat2<Term, Term>>>::Output: Nat2P1,
    <One<N> as NatRev>::Output: NatDivInternal<Two<D>, Nat2<Term, Term>>,
    One<N>: NatRev, 
• impl<N: Nat, D: Nat> NatRem<Zero<D>> for Two<N> where
    <<Two<N> as NatRev>::Output as NatDivInternal<Zero<D>, Nat2<Term, Term>>>::Output: Nat2P1,
    <Two<N> as NatRev>::Output: NatDivInternal<Zero<D>, Nat2<Term, Term>>,
    Two<N>: NatRev, 
• impl<N: Nat, D: Nat> NatRem<One<D>> for Two<N> where
    <<Two<N> as NatRev>::Output as NatDivInternal<One<D>, Nat2<Term, Term>>>::Output: Nat2P1,
    <Two<N> as NatRev>::Output: NatDivInternal<One<D>, Nat2<Term, Term>>,
    Two<N>: NatRev, 
• impl<N: Nat, D: Nat> NatRem<Two<D>> for Two<N> where
    <<Two<N> as NatRev>::Output as NatDivInternal<Two<D>, Nat2<Term, Term>>>::Output: Nat2P1,
    <Two<N> as NatRev>::Output: NatDivInternal<Two<D>, Nat2<Term, Term>>,
    Two<N>: NatRev,