TagLessEq

index_ext::tag

Struct TagLessEq 

Source 
pub struct TagLessEq<TagA, TagB> { /* private fields */ }
Expand description

A proof that the length if A is smaller or equal to B.

This guarantees that indices of A can also be used in B.

Implementations§

Source§

impl<A: Tag> TagLessEq<A, A>

Source

pub fn reflexive(tag: A) -> Self

Construct the reflexive proof.

Source§

impl<A: Tag, B: Tag> TagLessEq<A, B>

Source

pub fn with_sizes(a: ExactSize<A>, b: ExactSize<B>) -> Option<Self>

Construct the proof from the sizes of A and B.

Source

pub fn with_pair(a: Capacity<A>, b: Prefix<B>) -> Option<Self>

Construct the proof from a pair of bounds for A and B.

The Capacity upper bounds all indices applicable to A, and the exact size. The Prefix lower bounds all lengths and the exact size.

This returns Some when the lower bound for B is not smaller than the upper bound for A.

Trait Implementations§

Source§

impl<TagA: Clone, TagB: Clone> Clone for TagLessEq<TagA, TagB>

Source§

fn clone(&self) -> TagLessEq<TagA, TagB>

Returns a duplicate of the value. Read more
1.0.0 · Source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more
Source§

impl<TagA: Copy, TagB: Copy> Copy for TagLessEq<TagA, TagB>

Auto Trait Implementations§

§

impl<TagA, TagB> Freeze for TagLessEq<TagA, TagB>
where TagA: Freeze, TagB: Freeze,

§

impl<TagA, TagB> RefUnwindSafe for TagLessEq<TagA, TagB>
where TagA: RefUnwindSafe, TagB: RefUnwindSafe,

§

impl<TagA, TagB> Send for TagLessEq<TagA, TagB>
where TagA: Send, TagB: Send,

§

impl<TagA, TagB> Sync for TagLessEq<TagA, TagB>
where TagA: Sync, TagB: Sync,

§

impl<TagA, TagB> Unpin for TagLessEq<TagA, TagB>
where TagA: Unpin, TagB: Unpin,

§

impl<TagA, TagB> UnwindSafe for TagLessEq<TagA, TagB>
where TagA: UnwindSafe, TagB: 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> CloneToUninit for T
where T: Clone,

Source§

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)
Performs copy-assignment from self to dest. 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<T> ToOwned for T
where T: Clone,

Source§

type Owned = T

The resulting type after obtaining ownership.
Source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
Source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
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.