Trait NatUnique

pub trait NatUnique: Nat {
    type Output: Nat;
}

The Unique operator collapses one level of redundant zeroes in a ternary representation. Using Unique every time we might get a redundant zero should get rid of any potential problems with non-unique representations of zero.

Required Associated Types

type Output: Nat

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl NatUnique for Term

type Output = Term

impl NatUnique for Undefined

type Output = Undefined

impl NatUnique for Zero<Term>

type Output = Term

impl<N> NatUnique for Zero<One<N>>

where N: NatUnique + Nat,

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

impl<N> NatUnique for Zero<Two<N>>

where N: NatUnique + Nat,

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

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

type Output = One<N>

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

type Output = Two<N>

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

where Zero<N>: NatUnique,

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