type_level_logic::types::ternary

Struct One

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

Trait Implementations§

Source§

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

Source§

fn default() -> One<X>

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

impl<X: Nat> Nat for One<X>

Source§

fn reify() -> usize

Source§

impl<X: Nat> NatAdd<One<X>> for Term

Source§

type Output = One<X>

Source§

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

Source§

type Output = Undefined

Source§

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

Source§

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

Source§

impl<X, Y: Nat> NatAdd<One<Y>> for Two<X>
where <X as NatAdd<Y>>::Output: NatSucc, X: NatAdd<Y> + Nat,

Source§

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

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: Nat> NatAdd<Term> for One<X>

Source§

type Output = One<X>

Source§

impl<X, Y: Nat> NatAdd<Two<Y>> for One<X>
where <X as NatAdd<Y>>::Output: NatSucc, X: NatAdd<Y> + Nat,

Source§

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

Source§

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

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: Nat, L: Nat, E: Nat, G: Nat> NatCmp<One<X>, L, E, G> for Term

Source§

type Output = L

Source§

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

Source§

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

Source§

impl<X, Y: Nat, L: Nat, E: Nat, G: Nat> NatCmp<One<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<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: Nat, L: Nat, E: Nat, G: Nat> NatCmp<Term, L, E, G> for One<X>

Source§

type Output = G

Source§

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

Source§

type Output = <X as NatCmp<Y, L, L, 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<N: Nat, D: Nat> NatDiv<One<D>> for One<N>
where <<One<N> as NatRev>::Output as NatDivInternal<One<D>, Nat2<Term, Term>>>::Output: Nat2P2, <One<N> as NatRev>::Output: NatDivInternal<One<D>, Nat2<Term, Term>>, One<N>: NatRev,

Source§

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

Source§

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

Source§

type Output = Term

Source§

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

Source§

type Output = <<<Two<N> as NatRev>::Output as NatDivInternal<One<D>, Nat2<Term, Term>>>::Output as Nat2P2>::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 One<N>
where <<One<N> as NatRev>::Output as NatDivInternal<Two<D>, Nat2<Term, Term>>>::Output: Nat2P2, <One<N> as NatRev>::Output: NatDivInternal<Two<D>, Nat2<Term, Term>>, One<N>: NatRev,

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

type Output = Term

Source§

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

Source§

type Output = Undefined

Source§

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

Source§

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

Source§

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

Source§

type Output = <<One<X> as NatMul<One<Y>>>::Output as NatAdd<One<Y>>>::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 One<X>

Source§

type Output = Term

Source§

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

Source§

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

Source§

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

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> NatPred for One<X>
where X: NatTriple + Nat,

Source§

type Output = <X as NatTriple>::Output

Source§

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,

Source§

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

Source§

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

Source§

type Output = Term

Source§

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,

Source§

type Output = <<<Two<N> as NatRev>::Output as NatDivInternal<One<D>, Nat2<Term, Term>>>::Output as Nat2P1>::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 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,

Source§

type Output = <<<One<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<M, N: Nat> NatRevInternal<N> for One<M>
where M: NatRevInternal<One<N>> + Nat,

Source§

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

Source§

impl<X: Nat> NatSub<One<X>> for Term

Source§

type Output = Undefined

Source§

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

Source§

type Output = Undefined

Source§

impl<X, Y: Nat> NatSub<One<Y>> for One<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, Y: Nat> NatSub<One<Y>> for Two<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<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: Nat> NatSub<Term> for One<X>

Source§

type Output = One<X>

Source§

impl<X, Y: Nat> NatSub<Two<Y>> for One<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: Nat> NatSub<Undefined> for One<X>

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: Nat> NatSucc for One<X>

Source§

type Output = Two<X>

Source§

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

Source§

type Output = Zero<One<N>>

Source§

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

Source§

type Output = One<One<X>>

Source§

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

Source§

type Output = Two<One<X>>

Source§

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

Source§

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

Source§

impl<N: Nat> NatUnique for One<N>

Source§

type Output = One<N>

Auto Trait Implementations§

§

impl<X> Freeze for One<X>

§

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

§

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

§

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

§

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

§

impl<X> UnwindSafe for One<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,