Enum ExecMemContents 

pub enum ExecMemContents<T> {
    Uninit,
    Init(T),
}

MemContents<T> is compiled to ExecMemContents<T>

Variants

Uninit

Mirror of MemContents::Uninit

Init(T)

Mirror of MemContents::Init

Implementations

impl<T> ExecMemContents<T>

pub fn arrow_0(self) -> T

pub fn arrow_Init_0(self) -> T

impl<T: DeepView> ExecMemContents<T>

pub exec fn exec_is_Init(&self) -> res : bool

ensures

res == self.deep_view() is Init,

pub exec fn exec_is_Uninit(&self) -> res : bool

ensures

res == self.deep_view() is Uninit,

pub exec fn exec_arrow_Init_0(&self) -> res : &T

requires

self.deep_view() is Init,

ensures

res.deep_view() == self.deep_view()->Init_0,

pub exec fn exec_arrow_0(&self) -> res : &T

requires

self.deep_view() is Init,

ensures

res.deep_view() == self.deep_view()->0,

Trait Implementations

impl<T: Debug> Debug for ExecMemContents<T>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<T: DeepView> DeepView for ExecMemContents<T>

Implementations for shared traits

open spec fn deep_view(&self) -> Self::V

{
    match self {
        ExecMemContents::Uninit => MemContents::Uninit,
        ExecMemContents::Init(t) => MemContents::Init(t.deep_view()),
    }
}

type V = MemContents<<T as DeepView>::V>

impl<T: DeepViewClone> DeepViewClone for ExecMemContents<T>

exec fn deep_clone(&self) -> Self

impl<T: Eq> Eq for ExecMemContents<T>

impl<'a, T> ExecSpecMemContents<'a> for &'a ExecMemContents<T>

where T: DeepView + DeepViewClone,

Impls for MemContents methods

open spec fn is_init_spec(&self) -> bool

{ self.deep_view() is Init }

exec fn exec_is_init(self) -> res : bool

ensures

res == self.deep_view().is_init(),

exec fn exec_is_uninit(self) -> res : bool

ensures

res == self.deep_view().is_uninit(),

exec fn exec_value(self) -> res : Self::Elem

ensures

res.deep_view() == self.deep_view()->0,

type Elem = T

impl<T: Hash> Hash for ExecMemContents<T>

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl<T: ObeysDeepEq> ObeysDeepEq for ExecMemContents<T>

proof fn lemma_obeys_deep_eq()

impl<T: PartialEq> PartialEq for ExecMemContents<T>

fn eq(&self, other: &ExecMemContents<T>) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl<T: ObeysDeepEq> PartialEqSpecImpl for ExecMemContents<T>

Available on verus_keep_ghost only.

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &Self) -> bool

{ self.deep_view() == other.deep_view() }

impl<T: PartialEq> StructuralPartialEq for ExecMemContents<T>

impl<'a, T: DeepView + DeepViewClone> ToOwned<ExecMemContents<T>> for &'a ExecMemContents<T>

exec fn get_owned(self) -> ExecMemContents<T>

impl<'a, T: DeepView> ToRef<&'a ExecMemContents<T>> for &'a ExecMemContents<T>

exec fn get_ref(self) -> &'a ExecMemContents<T>