ResultAdditionalSpecFns

vstd::std_specs::result

Trait ResultAdditionalSpecFns

pub trait ResultAdditionalSpecFns<T, E> {
    // Required methods
    spec fn is_Ok(&self) -> bool;
    spec fn get_Ok_0(&self) -> T;
    spec fn arrow_Ok_0(&self) -> T;
    spec fn is_Err(&self) -> bool;
    spec fn get_Err_0(&self) -> E;
    spec fn arrow_Err_0(&self) -> E;
    proof fn tracked_unwrap(tracked self) -> tracked t : T;
    proof fn tracked_unwrap_err(tracked self) -> tracked t : E;
    proof fn tracked_expect(tracked self, msg: &str) -> tracked t : T;
    proof fn tracked_expect_err(tracked self, msg: &str) -> tracked t : E;
}

Required Methods§

spec fn is_Ok(&self) -> bool

👎Deprecated: is_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html

spec fn get_Ok_0(&self) -> T

👎Deprecated: get_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html

spec fn arrow_Ok_0(&self) -> T

spec fn is_Err(&self) -> bool

👎Deprecated: is_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html

spec fn get_Err_0(&self) -> E

👎Deprecated: get_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html

spec fn arrow_Err_0(&self) -> E

proof fn tracked_unwrap(tracked self) -> tracked t : T

requires

self.is_Ok(),

ensures

t == self->Ok_0,

proof fn tracked_unwrap_err(tracked self) -> tracked t : E

requires

self.is_Err(),

ensures

t == self->Err_0,

proof fn tracked_expect(tracked self, msg: &str) -> tracked t : T

requires

self.is_Ok(),

ensures

t == self->Ok_0,

proof fn tracked_expect_err(tracked self, msg: &str) -> tracked t : E

requires

self.is_Err(),

ensures

t == self->Err_0,

Implementations on Foreign Types§

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

open spec fn is_Ok(&self) -> bool

👎Deprecated: is_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html

{ is_variant(self, "Ok") }

open spec fn get_Ok_0(&self) -> T

👎Deprecated: get_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html

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

open spec fn arrow_Ok_0(&self) -> T

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

open spec fn is_Err(&self) -> bool

👎Deprecated: is_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html

{ is_variant(self, "Err") }

open spec fn get_Err_0(&self) -> E

👎Deprecated: get_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html

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

open spec fn arrow_Err_0(&self) -> E

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

proof fn tracked_unwrap(tracked self) -> tracked t : T

proof fn tracked_unwrap_err(tracked self) -> tracked t : E

proof fn tracked_expect(tracked self, msg: &str) -> tracked t : T

proof fn tracked_expect_err(tracked self, msg: &str) -> tracked t : E

Implementors§