type_level_logic::types::ternary

Struct Zero

Source 
pub struct Zero<X: Nat = Term>(/* private fields */);

Trait Implementations§

Source§

impl<X: Default + Nat> Default for Zero<X>

Source§

fn default() -> Zero<X>

Returns the “default value” for a type. Read more
Source§

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

Source§

fn reify() -> usize

Source§

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

Source§

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

Source§

impl<X> NatAdd<Term> for Zero<X>
where X: NatTriple + Nat,

Source§

type Output = <X as NatTriple>::Output

Source§

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

Source§

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

Source§

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

Source§

type Output = Undefined

Source§

impl<X> NatAdd<Zero<X>> for Term
where X: NatTriple + Nat,

Source§

type Output = <X as NatTriple>::Output

Source§

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

Source§

type Output = Undefined

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

impl<X, Y: Nat, L: Nat, E: Nat, G: Nat> NatCmp<One<Y>, L, E, G> for Zero<X>
where X: NatCmp<Y, L, L, G> + Nat,

Source§

type Output = <X as NatCmp<Y, L, L, G>>::Output

Source§

impl<X, L: Nat, E: Nat, G: Nat> NatCmp<Term, L, E, G> for Zero<X>
where X: NatCmp<Term, L, E, G> + Nat,

Source§

type Output = <X as NatCmp<Term, L, E, G>>::Output

Source§

impl<X, Y: Nat, L: Nat, E: Nat, G: Nat> NatCmp<Two<Y>, L, E, G> for Zero<X>
where X: NatCmp<Y, L, L, G> + Nat,

Source§

type Output = <X as NatCmp<Y, L, L, G>>::Output

Source§

impl<X: Nat, L: Nat, E: Nat, G: Nat> NatCmp<Zero<X>, L, E, G> for Term
where Term: NatCmp<X, L, E, G>,

Source§

type Output = <Term as NatCmp<X, L, E, G>>::Output

Source§

impl<X, Y: Nat, L: Nat, E: Nat, G: Nat> NatCmp<Zero<Y>, L, E, G> for One<X>
where X: NatCmp<Y, L, G, G> + Nat,

Source§

type Output = <X as NatCmp<Y, L, G, G>>::Output

Source§

impl<X, Y: Nat, L: Nat, E: Nat, G: Nat> NatCmp<Zero<Y>, L, E, G> for Two<X>
where X: NatCmp<Y, L, G, G> + Nat,

Source§

type Output = <X as NatCmp<Y, L, G, G>>::Output

Source§

impl<X, Y: Nat, L: Nat, E: Nat, G: Nat> NatCmp<Zero<Y>, L, E, G> for Zero<X>
where X: NatCmp<Y, L, E, G> + Nat,

Source§

type Output = <X as NatCmp<Y, L, E, G>>::Output

Source§

impl<N: Nat, D: Nat> NatDiv<One<D>> for Zero<N>
where <<Zero<N> as NatRev>::Output as NatDivInternal<One<D>, Nat2<Term, Term>>>::Output: Nat2P2, <Zero<N> as NatRev>::Output: NatDivInternal<One<D>, Nat2<Term, Term>>, Zero<N>: NatRev,

Source§

type Output = <<<Zero<N> as NatRev>::Output as NatDivInternal<One<D>, Nat2<Term, Term>>>::Output as Nat2P2>::Output

Source§

impl<N: Nat, D: Nat> NatDiv<Two<D>> for Zero<N>
where <<Zero<N> as NatRev>::Output as NatDivInternal<Two<D>, Nat2<Term, Term>>>::Output: Nat2P2, <Zero<N> as NatRev>::Output: NatDivInternal<Two<D>, Nat2<Term, Term>>, Zero<N>: NatRev,

Source§

type Output = <<<Zero<N> as NatRev>::Output as NatDivInternal<Two<D>, Nat2<Term, Term>>>::Output as Nat2P2>::Output

Source§

impl<N: Nat, D: Nat> NatDiv<Zero<D>> for One<N>
where <<One<N> as NatRev>::Output as NatDivInternal<Zero<D>, Nat2<Term, Term>>>::Output: Nat2P2, <One<N> as NatRev>::Output: NatDivInternal<Zero<D>, Nat2<Term, Term>>, One<N>: NatRev,

Source§

type Output = <<<One<N> as NatRev>::Output as NatDivInternal<Zero<D>, Nat2<Term, Term>>>::Output as Nat2P2>::Output

Source§

impl<D: Nat> NatDiv<Zero<D>> for Term

Source§

type Output = Term

Source§

impl<N: Nat, D: Nat> NatDiv<Zero<D>> for Two<N>
where <<Two<N> as NatRev>::Output as NatDivInternal<Zero<D>, Nat2<Term, Term>>>::Output: Nat2P2, <Two<N> as NatRev>::Output: NatDivInternal<Zero<D>, Nat2<Term, Term>>, Two<N>: NatRev,

Source§

type Output = <<<Two<N> as NatRev>::Output as NatDivInternal<Zero<D>, Nat2<Term, Term>>>::Output as Nat2P2>::Output

Source§

impl<N: Nat, D: Nat> NatDiv<Zero<D>> for Zero<N>
where <<Zero<N> as NatRev>::Output as NatDivInternal<Zero<D>, Nat2<Term, Term>>>::Output: Nat2P2, <Zero<N> as NatRev>::Output: NatDivInternal<Zero<D>, Nat2<Term, Term>>, Zero<N>: NatRev,

Source§

type Output = <<<Zero<N> as NatRev>::Output as NatDivInternal<Zero<D>, Nat2<Term, Term>>>::Output as Nat2P2>::Output

Source§

impl<N, D: Nat, R, Q> 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> + Nat, <<<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> + NatUndefOr2<One<Q>, Nat2<<R as NatTriple>::Output, <Q as NatTriple>::Output>>, <R as NatTriple>::Output: NatSub<D>, R: NatTriple + Nat, Q: NatTriple + Nat,

Source§

type Output = <N as 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>>::Output

Source§

impl<X> NatDoublePred for Zero<X>
where X: NatPred + Nat,

Source§

type Output = One<<X as NatPred>::Output>

Source§

impl<X, Y: Nat> NatMul<One<Y>> for Zero<X>
where X: NatMul<Zero<One<Y>>> + Nat,

Source§

type Output = <X as NatMul<Zero<One<Y>>>>::Output

Source§

impl<X: Nat> NatMul<Term> for Zero<X>

Source§

type Output = Term

Source§

impl<X, Y: Nat> NatMul<Two<Y>> for Zero<X>
where X: NatMul<Zero<Two<Y>>> + Nat,

Source§

type Output = <X as NatMul<Zero<Two<Y>>>>::Output

Source§

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

Source§

type Output = Undefined

Source§

impl<X: Nat> NatMul<Zero<X>> for Term

Source§

type Output = Term

Source§

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

Source§

type Output = Undefined

Source§

impl<X, Y: Nat> NatMul<Zero<Y>> for One<X>
where <X as NatMul<Zero<Zero<Y>>>>::Output: NatAdd<Zero<Y>>, X: NatMul<Zero<Zero<Y>>> + Nat,

Source§

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

Source§

impl<X: Nat, Y: Nat> NatMul<Zero<Y>> for Two<X>
where <One<X> as NatMul<Zero<Y>>>::Output: NatAdd<Zero<Y>>, One<X>: NatMul<Zero<Y>>,

Source§

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

Source§

impl<X, Y: Nat> NatMul<Zero<Y>> for Zero<X>
where X: NatMul<Zero<Zero<Y>>> + Nat,

Source§

type Output = <X as NatMul<Zero<Zero<Y>>>>::Output

Source§

impl<X> NatPred for Zero<X>
where X: NatPred + Nat,

Source§

type Output = Two<<X as NatPred>::Output>

Source§

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,

Source§

type Output = <<<Zero<N> as NatRev>::Output as NatDivInternal<One<D>, Nat2<Term, Term>>>::Output as Nat2P1>::Output

Source§

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,

Source§

type Output = <<<Zero<N> as NatRev>::Output as NatDivInternal<Two<D>, Nat2<Term, Term>>>::Output as Nat2P1>::Output

Source§

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,

Source§

type Output = <<<One<N> as NatRev>::Output as NatDivInternal<Zero<D>, Nat2<Term, Term>>>::Output as Nat2P1>::Output

Source§

impl<D: Nat> NatRem<Zero<D>> for Term

Source§

type Output = Term

Source§

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,

Source§

type Output = <<<Two<N> as NatRev>::Output as NatDivInternal<Zero<D>, Nat2<Term, Term>>>::Output as Nat2P1>::Output

Source§

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,

Source§

type Output = <<<Zero<N> as NatRev>::Output as NatDivInternal<Zero<D>, Nat2<Term, Term>>>::Output as Nat2P1>::Output

Source§

impl<M, N: Nat> NatRevInternal<N> for Zero<M>
where M: NatRevInternal<Zero<N>> + Nat,

Source§

type Output = <M as NatRevInternal<Zero<N>>>::Output

Source§

impl<X, Y: Nat> NatSub<One<Y>> for Zero<X>
where <<X as NatSub<Y>>::Output as NatPred>::Output: NatTriplePlusTwo, <X as NatSub<Y>>::Output: NatPred, X: NatSub<Y> + Nat,

Source§

type Output = <<<X as NatSub<Y>>::Output as NatPred>::Output as NatTriplePlusTwo>::Output

Source§

impl<X> NatSub<Term> for Zero<X>
where X: NatTriple + Nat,

Source§

type Output = <X as NatTriple>::Output

Source§

impl<X, Y: Nat> NatSub<Two<Y>> for Zero<X>
where <<X as NatSub<Y>>::Output as NatPred>::Output: NatTriplePlusOne, <X as NatSub<Y>>::Output: NatPred, X: NatSub<Y> + Nat,

Source§

type Output = <<<X as NatSub<Y>>::Output as NatPred>::Output as NatTriplePlusOne>::Output

Source§

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

Source§

type Output = Undefined

Source§

impl<X: Nat> NatSub<Zero<X>> for Term
where Term: NatSub<X>,

Source§

type Output = <Term as NatSub<X>>::Output

Source§

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

Source§

type Output = Undefined

Source§

impl<X, Y: Nat> NatSub<Zero<Y>> for One<X>
where <X as NatSub<Y>>::Output: NatTriplePlusOne, X: NatSub<Y> + Nat,

Source§

type Output = <<X as NatSub<Y>>::Output as NatTriplePlusOne>::Output

Source§

impl<X, Y: Nat> NatSub<Zero<Y>> for Two<X>
where <X as NatSub<Y>>::Output: NatTriplePlusTwo, X: NatSub<Y> + Nat,

Source§

type Output = <<X as NatSub<Y>>::Output as NatTriplePlusTwo>::Output

Source§

impl<X, Y: Nat> NatSub<Zero<Y>> for Zero<X>
where <X as NatSub<Y>>::Output: NatTriple, X: NatSub<Y> + Nat,

Source§

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

Source§

impl<X: Nat> NatSucc for Zero<X>

Source§

type Output = One<X>

Source§

impl<N: Nat> NatTriple for Zero<N>

Source§

type Output = Zero<Zero<N>>

Source§

impl<X: Nat> NatTriplePlusOne for Zero<X>

Source§

type Output = One<Zero<X>>

Source§

impl<X: Nat> NatTriplePlusTwo for Zero<X>

Source§

type Output = Two<Zero<X>>

Source§

impl<X: Nat, A: Nat, BC: NatPair> NatUndefOr2<A, BC> for Zero<X>

Source§

type Output = Nat2<Zero<X>, A>

Source§

impl NatUnique for Zero<Term>

Source§

type Output = Term

Source§

impl<N> NatUnique for Zero<One<N>>
where N: NatUnique + Nat,

Source§

type Output = Zero<One<<N as NatUnique>::Output>>

Source§

impl<N> NatUnique for Zero<Two<N>>
where N: NatUnique + Nat,

Source§

type Output = Zero<Two<<N as NatUnique>::Output>>

Source§

impl<N: Nat> NatUnique for Zero<Zero<N>>
where Zero<N>: NatUnique,

Source§

type Output = Zero<<Zero<N> as NatUnique>::Output>

Auto Trait Implementations§

§

impl<X> Freeze for Zero<X>

§

impl<X> RefUnwindSafe for Zero<X>
where X: RefUnwindSafe,

§

impl<X> Send for Zero<X>
where X: Send,

§

impl<X> Sync for Zero<X>
where X: Sync,

§

impl<X> Unpin for Zero<X>
where X: Unpin,

§

impl<X> UnwindSafe for Zero<X>
where X: UnwindSafe,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<N> NatRev for N
where N: Nat + NatRevInternal<Term>,

Source§

type Output = <N as NatRevInternal<Term>>::Output

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
Source§

impl<T> All for T
where T: ?Sized,