Struct CopyableStorageResource

pub struct CopyableStorageResource<K, V, P> { /* private fields */ }

Implementations§

A variant of StorageResource that implements Copy.

Use Self::into_resource to get the underlying resource.

The underlying value of the resource

The location of the resource

r.loc() == self.loc(),

r.value() == self.value(),

Trait Implementations§

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

{ true }

{ self }

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

Performs copy-assignment from self to dest. Read more

Returns the argument unchanged.

{ true }

{ v }

Calls U::from(self).

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

{ <U as FromSpec<Self>>::obeys_from_spec() }

{ <U as FromSpec<Self>>::from_spec(self) }

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.

{ <U as TryFromSpec<Self>>::obeys_try_from_spec() }

{ <U as TryFromSpec<Self>>::try_from_spec(self) }

Struct CopyableStorageResource Copy item path

Implementations§

impl<K, V, P: Protocol<K, V>> CopyableStorageResource<K, V, P>

pub uninterp spec fn value(self) -> P

pub uninterp spec fn loc(self) -> Loc

pub proof fn into_resource(self) -> r : StorageResource<K, V, P>

Trait Implementations§

impl<K, V, P> Clone for CopyableStorageResource<K, V, P>

exec fn clone(&self) -> Self

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

impl<K, V, P> Copy for CopyableStorageResource<K, V, P>

Auto Trait Implementations§

impl<K, V, P> Freeze for CopyableStorageResource<K, V, P>

impl<K, V, P> RefUnwindSafe for CopyableStorageResource<K, V, P>where K: RefUnwindSafe, V: RefUnwindSafe, P: RefUnwindSafe,

impl<K, V, P> Send for CopyableStorageResource<K, V, P>where K: Send + Sync, V: Send + Sync, P: Send,

impl<K, V, P> Sync for CopyableStorageResource<K, V, P>where K: Sync + Send, V: Sync + Send, P: Sync,

impl<K, V, P> Unpin for CopyableStorageResource<K, V, P>where K: Unpin, V: Unpin, P: Unpin,

impl<K, V, P> UnsafeUnpin for CopyableStorageResource<K, V, P>

impl<K, V, P> UnwindSafe for CopyableStorageResource<K, V, P>where K: UnwindSafe, V: UnwindSafe, P: 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<Borrowed, VERUS_SPEC__A> BorrowSpec<Borrowed> for VERUS_SPEC__Awhere VERUS_SPEC__A: Borrow<Borrowed> + ?Sized, Borrowed: ?Sized,

exec fn obeys_borrow_spec() -> bool

exec fn borrow_spec(&self) -> &Borrowed

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

open spec fn obeys_borrow_spec() -> bool

open spec fn borrow_spec(&self) -> &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>,

exec fn obeys_from_spec() -> bool

exec fn from_spec(v: T) -> VERUS_SPEC__A

impl<T> FromSpecImpl<T> for T

open spec fn obeys_from_spec() -> bool

open spec fn from_spec(v: T) -> T

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

exec fn obeys_into_spec() -> bool

exec fn into_spec(self) -> T

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

open spec fn obeys_into_spec() -> bool

open spec fn into_spec(self) -> U

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

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

exec fn obeys_try_from_spec() -> bool

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

exec fn obeys_try_into_spec() -> bool

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

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

open spec fn obeys_try_into_spec() -> bool

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

Struct CopyableStorageResource

impl<K, V, P> RefUnwindSafe for CopyableStorageResource<K, V, P>
where K: RefUnwindSafe, V: RefUnwindSafe, P: RefUnwindSafe,

impl<K, V, P> Send for CopyableStorageResource<K, V, P>
where K: Send + Sync, V: Send + Sync, P: Send,

impl<K, V, P> Sync for CopyableStorageResource<K, V, P>
where K: Sync + Send, V: Sync + Send, P: Sync,

impl<K, V, P> Unpin for CopyableStorageResource<K, V, P>
where K: Unpin, V: Unpin, P: Unpin,

impl<K, V, P> UnwindSafe for CopyableStorageResource<K, V, P>
where K: UnwindSafe, V: UnwindSafe, P: 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<Borrowed, VERUS_SPEC__A> BorrowSpec<Borrowed> for VERUS_SPEC__A
where VERUS_SPEC__A: Borrow<Borrowed> + ?Sized, Borrowed: ?Sized,

impl<T> BorrowSpecImpl<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<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,

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