Struct BiMap

pub struct BiMap<M, MRev>(pub M, pub MRev);

Tuple Fields§

§0: M§1: MRev

Implementations§

{
    let BiMap(m, mrev) = *self;
    m.spec_map(mrev.spec_map(o)) == o
}

{
    let BiMap(m, mrev) = *self;
    mrev.spec_map(m.spec_map(i)) == i
}

Trait Implementations§

call_ensures(M::clone, (&self.0,), cloned.0),

call_ensures(MRev::clone, (&self.1,), cloned.1),

Performs copy-assignment from source. Read more

Auto Trait Implementations§

Blanket Implementations§

Gets the TypeId of self. Read more

Immutably borrows from an owned value. Read more

Mutably borrows from an owned value. Read more

🔬This is a nightly-only experimental API. (clone_to_uninit)

Performs copy-assignment from self to dest. Read more

Returns the argument unchanged.

§

§

§

Calls U::from(self).

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

The resulting type after obtaining ownership.

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

Uses borrowed data to replace owned data, usually by cloning. Read more

The type returned in the event of a conversion error.

Performs the conversion.

§

§

§

The type returned in the event of a conversion error.

Performs the conversion.

Struct BiMap Copy item path

Tuple Fields§

Implementations§

impl<M, MRev> BiMap<M, MRev>where M: SpecMap, MRev: SpecMap<Input = M::Output, Output = M::Input>,

pub open spec fn sound(&self, o: M::Output) -> bool

pub open spec fn lossless(&self, i: M::Input) -> bool

Trait Implementations§

impl<M: Clone, MRev: Clone> Clone for BiMap<M, MRev>

exec fn clone(&self) -> cloned : Self

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

impl<M: Copy, MRev: Copy> Copy for BiMap<M, MRev>

Auto Trait Implementations§

impl<M, MRev> Freeze for BiMap<M, MRev>where M: Freeze, MRev: Freeze,

impl<M, MRev> RefUnwindSafe for BiMap<M, MRev>where M: RefUnwindSafe, MRev: RefUnwindSafe,

impl<M, MRev> Send for BiMap<M, MRev>where M: Send, MRev: Send,

impl<M, MRev> Sync for BiMap<M, MRev>where M: Sync, MRev: Sync,

impl<M, MRev> Unpin for BiMap<M, MRev>where M: Unpin, MRev: Unpin,

impl<M, MRev> UnsafeUnpin for BiMap<M, MRev>where M: UnsafeUnpin, MRev: UnsafeUnpin,

impl<M, MRev> UnwindSafe for BiMap<M, MRev>where M: UnwindSafe, MRev: UnwindSafe,

Blanket Implementations§

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

fn type_id(&self) -> TypeId

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

fn borrow(&self) -> &T

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

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

impl<T> CloneToUninit for Twhere T: Clone,

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

impl<T> From<T> for T

fn from(t: T) -> T

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__Awhere VERUS_SPEC__A: From<T>,

fn obeys_from_spec() -> bool

fn from_spec(v: T) -> VERUS_SPEC__A

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

fn into(self) -> U

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__Awhere VERUS_SPEC__A: Into<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> T

impl<T, U> IntoSpecImpl<U> for Twhere U: From<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> U

impl<T> ToOwned for Twhere T: Clone,

type Owned = T

fn to_owned(&self) -> T

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

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

type Error = Infallible

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

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__Awhere VERUS_SPEC__A: TryFrom<T>,

fn obeys_try_from_spec() -> bool

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

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

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

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

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__Awhere VERUS_SPEC__A: TryInto<T>,

fn obeys_try_into_spec() -> bool

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

impl<T, U> TryIntoSpecImpl<U> for Twhere U: TryFrom<T>,

fn obeys_try_into_spec() -> bool

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

impl<A> SpecEq<&A> for Awhere A: ?Sized,

impl<A> SpecEq<&mut A> for Awhere A: ?Sized,

impl<A> SpecEq<A> for Awhere A: ?Sized,

impl<A> SpecEq<Ghost<A>> for A

impl<A> SpecEq<Tracked<A>> for A

Struct BiMap

impl<M, MRev> BiMap<M, MRev>
where M: SpecMap, MRev: SpecMap<Input = M::Output, Output = M::Input>,

impl<M, MRev> Freeze for BiMap<M, MRev>
where M: Freeze, MRev: Freeze,

impl<M, MRev> RefUnwindSafe for BiMap<M, MRev>
where M: RefUnwindSafe, MRev: RefUnwindSafe,

impl<M, MRev> Send for BiMap<M, MRev>
where M: Send, MRev: Send,

impl<M, MRev> Sync for BiMap<M, MRev>
where M: Sync, MRev: Sync,

impl<M, MRev> Unpin for BiMap<M, MRev>
where M: Unpin, MRev: Unpin,

impl<M, MRev> UnsafeUnpin for BiMap<M, MRev>
where M: UnsafeUnpin, MRev: UnsafeUnpin,

impl<M, MRev> UnwindSafe for BiMap<M, MRev>
where M: UnwindSafe, MRev: UnwindSafe,

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

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

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

impl<T> CloneToUninit for T
where T: Clone,

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

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

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

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

impl<T> ToOwned for T
where T: Clone,

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

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

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

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

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

impl<A> SpecEq<&A> for A
where A: ?Sized,

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

impl<A> SpecEq<A> for A
where A: ?Sized,