Trait ExecSpecOptionUnwrap 

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;
}

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

Required Associated Types

type Elem: DeepView + DeepViewClone

Required Methods

spec fn is_some_spec(&self) -> bool

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".

Implementations on Foreign Types

impl<'a, T> ExecSpecOptionUnwrap<'a> for &'a Option<T>

where T: DeepView + DeepViewClone,

Impls for Option methods

open spec fn is_some_spec(&self) -> bool

{ self.is_some() }

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

ensures

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

type Elem = T

Implementors