Trait ExecSpecResultArrow 

pub trait ExecSpecResultArrow<T, E>: Sized {
    // Required methods
    spec fn is_ok_variant_spec(&self) -> bool;
    spec fn is_err_variant_spec(&self) -> bool;
    exec fn exec_arrow_Ok_0(&self) -> &T;
    exec fn exec_arrow_Err_0(&self) -> &E;
}

Required Methods

spec fn is_ok_variant_spec(&self) -> bool

spec fn is_err_variant_spec(&self) -> bool

exec fn exec_arrow_Ok_0(&self) -> &T

requires

self.is_ok_variant_spec(),

exec fn exec_arrow_Err_0(&self) -> &E

requires

self.is_err_variant_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<T: DeepView, E: DeepView> ExecSpecResultArrow<T, E> for Result<T, E>

open spec fn is_ok_variant_spec(&self) -> bool

{ *self is Ok }

open spec fn is_err_variant_spec(&self) -> bool

{ *self is Err }

exec fn exec_arrow_Ok_0(&self) -> res : &T

ensures

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

exec fn exec_arrow_Err_0(&self) -> res : &E

ensures

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

Implementors