Trait type_level_logic::strong::ternary::NatDivInternal

pub trait NatDivInternal<B: Nat, C: NatPair>: Nat {
    type Output: NatPair;
}

Associated Types

type Output: NatPair

Implementors

• impl<D: Nat, RQ: NatPair> NatDivInternal<D, RQ> for Term
• impl<N: Nat, D: Nat, R: Nat, Q: Nat> NatDivInternal<D, Nat2<R, Q>> for Zero<N> where
    N: NatDivInternal<D, <<<<R as NatTriple>::Output as NatSub<D>>::Output as NatSub<D>>::Output as NatUndefOr2<Two<Q>, <<<R as NatTriple>::Output as NatSub<D>>::Output as NatUndefOr2<One<Q>, Nat2<<R as NatTriple>::Output, <Q as NatTriple>::Output>>>::Output>>::Output>,
    <<<R as NatTriple>::Output as NatSub<D>>::Output as NatSub<D>>::Output: NatUndefOr2<Two<Q>, <<<R as NatTriple>::Output as NatSub<D>>::Output as NatUndefOr2<One<Q>, Nat2<<R as NatTriple>::Output, <Q as NatTriple>::Output>>>::Output>,
    <<R as NatTriple>::Output as NatSub<D>>::Output: NatSub<D>,
    <R as NatTriple>::Output: NatSub<D>,
    R: NatTriple,
    <<R as NatTriple>::Output as NatSub<D>>::Output: NatUndefOr2<One<Q>, Nat2<<R as NatTriple>::Output, <Q as NatTriple>::Output>>,
    <R as NatTriple>::Output: NatSub<D>,
    R: NatTriple,
    R: NatTriple,
    Q: NatTriple, 
• impl<N: Nat, D: Nat, R: Nat, Q: Nat> NatDivInternal<D, Nat2<R, Q>> for One<N> where
    N: NatDivInternal<D, <<<One<R> as NatSub<D>>::Output as NatSub<D>>::Output as NatUndefOr2<Two<Q>, <<One<R> as NatSub<D>>::Output as NatUndefOr2<One<Q>, Nat2<One<R>, <Q as NatTriple>::Output>>>::Output>>::Output>,
    <<One<R> as NatSub<D>>::Output as NatSub<D>>::Output: NatUndefOr2<Two<Q>, <<One<R> as NatSub<D>>::Output as NatUndefOr2<One<Q>, Nat2<One<R>, <Q as NatTriple>::Output>>>::Output>,
    <One<R> as NatSub<D>>::Output: NatSub<D>,
    One<R>: NatSub<D>,
    <One<R> as NatSub<D>>::Output: NatUndefOr2<One<Q>, Nat2<One<R>, <Q as NatTriple>::Output>>,
    One<R>: NatSub<D>,
    Q: NatTriple, 
• impl<N: Nat, D: Nat, R: Nat, Q: Nat> NatDivInternal<D, Nat2<R, Q>> for Two<N> where
    N: NatDivInternal<D, <<<Two<R> as NatSub<D>>::Output as NatSub<D>>::Output as NatUndefOr2<Two<Q>, <<Two<R> as NatSub<D>>::Output as NatUndefOr2<One<Q>, Nat2<Two<R>, <Q as NatTriple>::Output>>>::Output>>::Output>,
    <<Two<R> as NatSub<D>>::Output as NatSub<D>>::Output: NatUndefOr2<Two<Q>, <<Two<R> as NatSub<D>>::Output as NatUndefOr2<One<Q>, Nat2<Two<R>, <Q as NatTriple>::Output>>>::Output>,
    <Two<R> as NatSub<D>>::Output: NatSub<D>,
    Two<R>: NatSub<D>,
    <Two<R> as NatSub<D>>::Output: NatUndefOr2<One<Q>, Nat2<Two<R>, <Q as NatTriple>::Output>>,
    Two<R>: NatSub<D>,
    Q: NatTriple,