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;
}Required Methods§
Sourcespec 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 is_Ok(&self) -> bool
-> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.htmlSourcespec 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 get_Ok_0(&self) -> T
-> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.htmlSourcespec fn arrow_Ok_0(&self) -> T
spec fn arrow_Ok_0(&self) -> T
Sourcespec 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 is_Err(&self) -> bool
-> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.htmlSourcespec 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 get_Err_0(&self) -> E
-> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.htmlSourcespec fn arrow_Err_0(&self) -> E
spec fn arrow_Err_0(&self) -> E
Implementations on Foreign Types§
Source§impl<T, E> ResultAdditionalSpecFns<T, E> for Result<T, E>
impl<T, E> ResultAdditionalSpecFns<T, E> for Result<T, E>
Source§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
open spec fn is_Ok(&self) -> bool
-> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html{ is_variant(self, "Ok") }Source§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
open spec fn get_Ok_0(&self) -> T
-> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html{ get_variant_field(self, "Ok", "0") }Source§open spec fn arrow_Ok_0(&self) -> T
open spec fn arrow_Ok_0(&self) -> T
{ get_variant_field(self, "Ok", "0") }Source§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
open spec fn is_Err(&self) -> bool
-> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html{ is_variant(self, "Err") }Source§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
open spec fn get_Err_0(&self) -> E
-> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html{ get_variant_field(self, "Err", "0") }Source§open spec fn arrow_Err_0(&self) -> E
open spec fn arrow_Err_0(&self) -> E
{ get_variant_field(self, "Err", "0") }