Trait vstd::std_specs::result::ResultAdditionalSpecFns

source · 
pub trait ResultAdditionalSpecFns<T, E> {
    // Required methods
    spec fn is_Ok(&self) -> bool;
    spec fn get_Ok_0(&self) -> T;
    spec fn is_Err(&self) -> bool;
    spec fn get_Err_0(&self) -> E;
}

Required Methods§

source

spec fn is_Ok(&self) -> bool

source

spec fn get_Ok_0(&self) -> T

source

spec fn is_Err(&self) -> bool

source

spec fn get_Err_0(&self) -> E

Implementations on Foreign Types§

source§

impl<T, E> ResultAdditionalSpecFns<T, E> for Result<T, E>

source§

open spec fn is_Ok(&self) -> bool

{ is_variant(self, "Ok") }
source§

open spec fn get_Ok_0(&self) -> T

{ get_variant_field(self, "Ok", "0") }
source§

open spec fn is_Err(&self) -> bool

{ is_variant(self, "Err") }
source§

open spec fn get_Err_0(&self) -> E

{ get_variant_field(self, "Err", "0") }

Implementors§