type_level_logic::types::balanced

Struct Minus

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

Trait Implementations§

Source§

impl<X: Default + Int> Default for Minus<X>

Source§

fn default() -> Minus<X>

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

impl<X: Int> Int for Minus<X>

Source§

fn reify() -> isize

Source§

impl<X: Int> IntAbs for Minus<X>
where Term: IntLteCmp<Minus<X>, Minus<X>, <Minus<X> as IntNeg>::Output>, Minus<X>: IntNeg,

Source§

type Output = <Term as IntLteCmp<Minus<X>, Minus<X>, <Minus<X> as IntNeg>::Output>>::Output

Source§

impl<M, N: Int> IntAdd<Minus<N>> for Minus<M>
where <M as IntAdd<N>>::Output: IntAdd<Minus>, M: IntAdd<N> + Int,

Source§

type Output = Plus<<<M as IntAdd<N>>::Output as IntAdd<Minus>>::Output>

Source§

impl<M, N: Int> IntAdd<Minus<N>> for Plus<M>
where Zero<<M as IntAdd<N>>::Output>: Unique, M: IntAdd<N> + Int,

Source§

type Output = <Zero<<M as IntAdd<N>>::Output> as Unique>::Output

Source§

impl<N: Int> IntAdd<Minus<N>> for Term

Source§

type Output = Minus<N>

Source§

impl<N: Int> IntAdd<Minus<N>> for Undefined

Source§

type Output = Undefined

Source§

impl<M, N: Int> IntAdd<Minus<N>> for Zero<M>
where M: IntAdd<N> + Int,

Source§

type Output = Minus<<M as IntAdd<N>>::Output>

Source§

impl<M, N: Int> IntAdd<Plus<N>> for Minus<M>
where Zero<<M as IntAdd<N>>::Output>: Unique, M: IntAdd<N> + Int,

Source§

type Output = <Zero<<M as IntAdd<N>>::Output> as Unique>::Output

Source§

impl<N: Int> IntAdd<Term> for Minus<N>

Source§

type Output = Minus<N>

Source§

impl<N: Int> IntAdd<Undefined> for Minus<N>

Source§

type Output = Undefined

Source§

impl<M, N: Int> IntAdd<Zero<N>> for Minus<M>
where M: IntAdd<N> + Int,

Source§

type Output = Minus<<M as IntAdd<N>>::Output>

Source§

impl<M, N: Int, L: Int, E: Int, G: Int> IntCmp<Minus<N>, L, E, G> for Minus<M>
where M: IntCmp<N, L, E, G> + Int,

Source§

type Output = <M as IntCmp<N, L, E, G>>::Output

Source§

impl<M, N: Int, L: Int, E: Int, G: Int> IntCmp<Minus<N>, L, E, G> for Plus<M>
where M: IntCmp<N, L, G, G> + Int,

Source§

type Output = <M as IntCmp<N, L, G, G>>::Output

Source§

impl<N: Int, L: Int, E: Int, G: Int> IntCmp<Minus<N>, L, E, G> for Term
where Term: IntCmp<N, L, G, G>,

Source§

type Output = <Term as IntCmp<N, L, G, G>>::Output

Source§

impl<M, N: Int, L: Int, E: Int, G: Int> IntCmp<Minus<N>, L, E, G> for Zero<M>
where M: IntCmp<N, L, G, G> + Int,

Source§

type Output = <M as IntCmp<N, L, G, G>>::Output

Source§

impl<M, N: Int, L: Int, E: Int, G: Int> IntCmp<Plus<N>, L, E, G> for Minus<M>
where M: IntCmp<N, L, L, G> + Int,

Source§

type Output = <M as IntCmp<N, L, L, G>>::Output

Source§

impl<N, L: Int, E: Int, G: Int> IntCmp<Term, L, E, G> for Minus<N>
where N: IntCmp<Term, L, L, G> + Int,

Source§

type Output = <N as IntCmp<Term, L, L, G>>::Output

Source§

impl<M, N: Int, L: Int, E: Int, G: Int> IntCmp<Zero<N>, L, E, G> for Minus<M>
where M: IntCmp<N, L, L, G> + Int,

Source§

type Output = <M as IntCmp<N, L, L, G>>::Output

Source§

impl<M, N: Int, L: IntPair, E: IntPair, G: IntPair> IntCmp2<Minus<N>, L, E, G> for Minus<M>
where M: IntCmp2<N, L, E, G> + Int,

Source§

type Output = <M as IntCmp2<N, L, E, G>>::Output

Source§

impl<M, N: Int, L: IntPair, E: IntPair, G: IntPair> IntCmp2<Minus<N>, L, E, G> for Plus<M>
where M: IntCmp2<N, L, G, G> + Int,

Source§

type Output = <M as IntCmp2<N, L, G, G>>::Output

Source§

impl<N: Int, L: IntPair, E: IntPair, G: IntPair> IntCmp2<Minus<N>, L, E, G> for Term
where Term: IntCmp2<N, L, G, G>,

Source§

type Output = <Term as IntCmp2<N, L, G, G>>::Output

Source§

impl<M, N: Int, L: IntPair, E: IntPair, G: IntPair> IntCmp2<Minus<N>, L, E, G> for Zero<M>
where M: IntCmp2<N, L, G, G> + Int,

Source§

type Output = <M as IntCmp2<N, L, G, G>>::Output

Source§

impl<M, N: Int, L: IntPair, E: IntPair, G: IntPair> IntCmp2<Plus<N>, L, E, G> for Minus<M>
where M: IntCmp2<N, L, L, G> + Int,

Source§

type Output = <M as IntCmp2<N, L, L, G>>::Output

Source§

impl<N, L: IntPair, E: IntPair, G: IntPair> IntCmp2<Term, L, E, G> for Minus<N>
where N: IntCmp2<Term, L, L, G> + Int,

Source§

type Output = <N as IntCmp2<Term, L, L, G>>::Output

Source§

impl<M, N: Int, L: IntPair, E: IntPair, G: IntPair> IntCmp2<Zero<N>, L, E, G> for Minus<M>
where M: IntCmp2<N, L, L, G> + Int,

Source§

type Output = <M as IntCmp2<N, L, L, G>>::Output

Source§

impl<N: Int, D: Int> IntDiv<Minus<D>> for Minus<N>
where <<Minus<N> as IntRev>::Output as IntDivInternal<Minus<D>, Int2<Term, Term>>>::Output: Int2P2, <Minus<N> as IntRev>::Output: IntDivInternal<Minus<D>, Int2<Term, Term>>, Minus<N>: IntRev,

Source§

type Output = <<<Minus<N> as IntRev>::Output as IntDivInternal<Minus<D>, Int2<Term, Term>>>::Output as Int2P2>::Output

Source§

impl<N: Int, D: Int> IntDiv<Minus<D>> for Plus<N>
where <<Plus<N> as IntRev>::Output as IntDivInternal<Minus<D>, Int2<Term, Term>>>::Output: Int2P2, <Plus<N> as IntRev>::Output: IntDivInternal<Minus<D>, Int2<Term, Term>>, Plus<N>: IntRev,

Source§

type Output = <<<Plus<N> as IntRev>::Output as IntDivInternal<Minus<D>, Int2<Term, Term>>>::Output as Int2P2>::Output

Source§

impl<D: Int> IntDiv<Minus<D>> for Term

Source§

type Output = Term

Source§

impl<N: Int, D: Int> IntDiv<Minus<D>> for Zero<N>
where <<Zero<N> as IntRev>::Output as IntDivInternal<Minus<D>, Int2<Term, Term>>>::Output: Int2P2, <Zero<N> as IntRev>::Output: IntDivInternal<Minus<D>, Int2<Term, Term>>, Zero<N>: IntRev,

Source§

type Output = <<<Zero<N> as IntRev>::Output as IntDivInternal<Minus<D>, Int2<Term, Term>>>::Output as Int2P2>::Output

Source§

impl<N: Int, D: Int> IntDiv<Plus<D>> for Minus<N>
where <<Minus<N> as IntRev>::Output as IntDivInternal<Plus<D>, Int2<Term, Term>>>::Output: Int2P2, <Minus<N> as IntRev>::Output: IntDivInternal<Plus<D>, Int2<Term, Term>>, Minus<N>: IntRev,

Source§

type Output = <<<Minus<N> as IntRev>::Output as IntDivInternal<Plus<D>, Int2<Term, Term>>>::Output as Int2P2>::Output

Source§

impl<N: Int, D: Int> IntDiv<Zero<D>> for Minus<N>
where <<Minus<N> as IntRev>::Output as IntDivInternal<Zero<D>, Int2<Term, Term>>>::Output: Int2P2, <Minus<N> as IntRev>::Output: IntDivInternal<Zero<D>, Int2<Term, Term>>, Minus<N>: IntRev,

Source§

type Output = <<<Minus<N> as IntRev>::Output as IntDivInternal<Zero<D>, Int2<Term, Term>>>::Output as Int2P2>::Output

Source§

impl<N, D: Int, R: Int, Q> IntDivInternal<D, Int2<R, Q>> for Minus<N>
where N: IntDivInternal<D, <Minus<R> as IntAbsMinThreeCmp<<Minus<R> as IntSub<D>>::Output, <Minus<R> as IntAdd<D>>::Output, <Q as IntTriple>::Output, Plus<Q>, Minus<Q>>>::Output> + Int, Minus<R>: IntAbsMinThreeCmp<<Minus<R> as IntSub<D>>::Output, <Minus<R> as IntAdd<D>>::Output, <Q as IntTriple>::Output, Plus<Q>, Minus<Q>> + IntSub<D> + IntAdd<D>, Q: IntTriple + Int,

Source§

type Output = <N as IntDivInternal<D, <Minus<R> as IntAbsMinThreeCmp<<Minus<R> as IntSub<D>>::Output, <Minus<R> as IntAdd<D>>::Output, <Q as IntTriple>::Output, Plus<Q>, Minus<Q>>>::Output>>::Output

Source§

impl<M, N: Int> IntMul<Minus<N>> for Minus<M>
where <M as IntMul<Zero<Minus<N>>>>::Output: IntSub<Minus<N>>, M: IntMul<Zero<Minus<N>>> + Int,

Source§

type Output = <<M as IntMul<Zero<Minus<N>>>>::Output as IntSub<Minus<N>>>::Output

Source§

impl<M, N: Int> IntMul<Minus<N>> for Plus<M>
where <M as IntMul<Zero<Minus<N>>>>::Output: IntAdd<Minus<N>>, M: IntMul<Zero<Minus<N>>> + Int,

Source§

type Output = <<M as IntMul<Zero<Minus<N>>>>::Output as IntAdd<Minus<N>>>::Output

Source§

impl<N: Int> IntMul<Minus<N>> for Term

Source§

type Output = Term

Source§

impl<N: Int> IntMul<Minus<N>> for Undefined

Source§

type Output = Undefined

Source§

impl<M, N: Int> IntMul<Minus<N>> for Zero<M>
where M: IntMul<Zero<Minus<N>>> + Int,

Source§

type Output = <M as IntMul<Zero<Minus<N>>>>::Output

Source§

impl<M, N: Int> IntMul<Plus<N>> for Minus<M>
where <M as IntMul<Zero<Plus<N>>>>::Output: IntSub<Plus<N>>, M: IntMul<Zero<Plus<N>>> + Int,

Source§

type Output = <<M as IntMul<Zero<Plus<N>>>>::Output as IntSub<Plus<N>>>::Output

Source§

impl<N: Int> IntMul<Term> for Minus<N>

Source§

type Output = Term

Source§

impl<N: Int> IntMul<Undefined> for Minus<N>

Source§

type Output = Undefined

Source§

impl<M, N: Int> IntMul<Zero<N>> for Minus<M>
where <M as IntMul<Zero<Zero<N>>>>::Output: IntSub<Zero<N>>, M: IntMul<Zero<Zero<N>>> + Int,

Source§

type Output = <<M as IntMul<Zero<Zero<N>>>>::Output as IntSub<Zero<N>>>::Output

Source§

impl<N> IntNeg for Minus<N>
where N: IntNeg + Int,

Source§

type Output = Plus<<N as IntNeg>::Output>

Source§

impl<N> IntPred for Minus<N>
where N: IntPred + Int,

Source§

type Output = Plus<<N as IntPred>::Output>

Source§

impl<N: Int, D: Int> IntRem<Minus<D>> for Minus<N>
where <<Minus<N> as IntRev>::Output as IntDivInternal<Minus<D>, Int2<Term, Term>>>::Output: Int2P1, <Minus<N> as IntRev>::Output: IntDivInternal<Minus<D>, Int2<Term, Term>>, Minus<N>: IntRev,

Source§

type Output = <<<Minus<N> as IntRev>::Output as IntDivInternal<Minus<D>, Int2<Term, Term>>>::Output as Int2P1>::Output

Source§

impl<N: Int, D: Int> IntRem<Minus<D>> for Plus<N>
where <<Plus<N> as IntRev>::Output as IntDivInternal<Minus<D>, Int2<Term, Term>>>::Output: Int2P1, <Plus<N> as IntRev>::Output: IntDivInternal<Minus<D>, Int2<Term, Term>>, Plus<N>: IntRev,

Source§

type Output = <<<Plus<N> as IntRev>::Output as IntDivInternal<Minus<D>, Int2<Term, Term>>>::Output as Int2P1>::Output

Source§

impl<D: Int> IntRem<Minus<D>> for Term

Source§

type Output = Term

Source§

impl<N: Int, D: Int> IntRem<Minus<D>> for Zero<N>
where <<Zero<N> as IntRev>::Output as IntDivInternal<Minus<D>, Int2<Term, Term>>>::Output: Int2P1, <Zero<N> as IntRev>::Output: IntDivInternal<Minus<D>, Int2<Term, Term>>, Zero<N>: IntRev,

Source§

type Output = <<<Zero<N> as IntRev>::Output as IntDivInternal<Minus<D>, Int2<Term, Term>>>::Output as Int2P1>::Output

Source§

impl<N: Int, D: Int> IntRem<Plus<D>> for Minus<N>
where <<Minus<N> as IntRev>::Output as IntDivInternal<Plus<D>, Int2<Term, Term>>>::Output: Int2P1, <Minus<N> as IntRev>::Output: IntDivInternal<Plus<D>, Int2<Term, Term>>, Minus<N>: IntRev,

Source§

type Output = <<<Minus<N> as IntRev>::Output as IntDivInternal<Plus<D>, Int2<Term, Term>>>::Output as Int2P1>::Output

Source§

impl<N: Int, D: Int> IntRem<Zero<D>> for Minus<N>
where <<Minus<N> as IntRev>::Output as IntDivInternal<Zero<D>, Int2<Term, Term>>>::Output: Int2P1, <Minus<N> as IntRev>::Output: IntDivInternal<Zero<D>, Int2<Term, Term>>, Minus<N>: IntRev,

Source§

type Output = <<<Minus<N> as IntRev>::Output as IntDivInternal<Zero<D>, Int2<Term, Term>>>::Output as Int2P1>::Output

Source§

impl<M, N: Int> IntRevInternal<N> for Minus<M>
where M: IntRevInternal<Minus<N>> + Int,

Source§

type Output = <M as IntRevInternal<Minus<N>>>::Output

Source§

impl<M, N: Int> IntSub<Minus<N>> for Minus<M>
where Zero<<M as IntSub<N>>::Output>: Unique, M: IntSub<N> + Int,

Source§

type Output = <Zero<<M as IntSub<N>>::Output> as Unique>::Output

Source§

impl<M, N: Int> IntSub<Minus<N>> for Plus<M>
where <M as IntSub<N>>::Output: IntSub<Minus>, M: IntSub<N> + Int,

Source§

type Output = Minus<<<M as IntSub<N>>::Output as IntSub<Minus>>::Output>

Source§

impl<N> IntSub<Minus<N>> for Term
where N: IntNeg + Int,

Source§

type Output = Plus<<N as IntNeg>::Output>

Source§

impl<N: Int> IntSub<Minus<N>> for Undefined

Source§

type Output = Undefined

Source§

impl<M, N: Int> IntSub<Minus<N>> for Zero<M>
where M: IntSub<N> + Int,

Source§

type Output = Plus<<M as IntSub<N>>::Output>

Source§

impl<M, N: Int> IntSub<Plus<N>> for Minus<M>
where <M as IntSub<N>>::Output: IntSub<Plus>, M: IntSub<N> + Int,

Source§

type Output = Plus<<<M as IntSub<N>>::Output as IntSub<Plus>>::Output>

Source§

impl<N: Int> IntSub<Term> for Minus<N>

Source§

type Output = Minus<N>

Source§

impl<N: Int> IntSub<Undefined> for Minus<N>

Source§

type Output = Undefined

Source§

impl<M, N: Int> IntSub<Zero<N>> for Minus<M>
where M: IntSub<N> + Int,

Source§

type Output = Minus<<M as IntSub<N>>::Output>

Source§

impl<N: Int> IntSucc for Minus<N>
where Zero<N>: Unique,

Source§

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

Source§

impl<N: Int> IntTriple for Minus<N>

Source§

type Output = Zero<Minus<N>>

Source§

impl<N: Int> Unique for Minus<N>

Source§

type Output = Minus<N>

Auto Trait Implementations§

§

impl<X> Freeze for Minus<X>

§

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

§

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

§

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

§

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

§

impl<X> UnwindSafe for Minus<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<X, Y, Z, A, B, C> IntAbsMinThreeCmp<Y, Z, A, B, C> for X
where X: Int + IntAbs, Y: Int + IntAbs, Z: Int + IntAbs, A: Int, B: Int, C: Int, <Y as IntAbs>::Output: IntLteCmp2<<Z as IntAbs>::Output, <<X as IntAbs>::Output as IntLteCmp2<<Y as IntAbs>::Output, Int2<X, A>, Int2<Y, B>>>::Output, <<X as IntAbs>::Output as IntLteCmp2<<Z as IntAbs>::Output, Int2<X, A>, Int2<Z, C>>>::Output>, <X as IntAbs>::Output: IntLteCmp2<<Y as IntAbs>::Output, Int2<X, A>, Int2<Y, B>> + IntLteCmp2<<Z as IntAbs>::Output, Int2<X, A>, Int2<Z, C>>,

Source§

type Output = <<Y as IntAbs>::Output as IntLteCmp2<<Z as IntAbs>::Output, <<X as IntAbs>::Output as IntLteCmp2<<Y as IntAbs>::Output, Int2<X, A>, Int2<Y, B>>>::Output, <<X as IntAbs>::Output as IntLteCmp2<<Z as IntAbs>::Output, Int2<X, A>, Int2<Z, C>>>::Output>>::Output

Source§

impl<X, Y, LE, G> IntLteCmp<Y, LE, G> for X
where X: Int + IntCmp<Y, LE, LE, G>, Y: Int, LE: Int, G: Int,

Source§

type Output = <X as IntCmp<Y, LE, LE, G>>::Output

Source§

impl<X, Y, LE, G> IntLteCmp2<Y, LE, G> for X
where X: Int + IntCmp2<Y, LE, LE, G>, Y: Int, LE: IntPair, G: IntPair,

Source§

type Output = <X as IntCmp2<Y, LE, LE, G>>::Output

Source§

impl<N> IntRev for N
where N: Int + IntRevInternal<Term>,

Source§

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

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<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,