ExecSpecOptionUnwrap

vstd::contrib::exec_spec

Trait ExecSpecOptionUnwrap 

Source 
pub trait ExecSpecOptionUnwrap<'a>: Sized + DeepView {
    type Elem: DeepView + DeepViewClone;

    // Required methods
    spec fn is_some_spec(&self) -> bool;
    exec fn exec_unwrap(self) -> Self::Elem;
}
Expand description

Traits for Option methods Spec for executable version of Option::unwrap.

Required Associated Types§

Source

type Elem: DeepView + DeepViewClone

Required Methods§

Source

spec fn is_some_spec(&self) -> bool

Source

exec fn exec_unwrap(self) -> Self::Elem

requires
self.is_some_spec(),

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.

Implementations on Foreign Types§

Source§

impl<'a, T> ExecSpecOptionUnwrap<'a> for &'a Option<T>
where T: DeepView + DeepViewClone,

Impls for Option methods

Source§

open spec fn is_some_spec(&self) -> bool

{ self.is_some() }
Source§

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

ensures
res.deep_view() == self.deep_view()->0,
Source§

type Elem = T

Implementors§