pub trait OptionAdditionalFns<T>: Sized {
// Required methods
spec fn is_Some(&self) -> bool;
spec fn get_Some_0(&self) -> T;
spec fn is_None(&self) -> bool;
spec fn arrow_Some_0(&self) -> T;
spec fn arrow_0(&self) -> T;
proof fn tracked_unwrap(tracked self) -> tracked t : T;
proof fn tracked_expect(tracked self, msg: &str) -> tracked t : T;
proof fn tracked_borrow(tracked &self) -> tracked t : &T;
proof fn tracked_take(tracked &mut self) -> tracked t : T;
}Required Methods§
Sourcespec fn is_Some(&self) -> bool
👎Deprecated: is_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html
spec fn is_Some(&self) -> bool
is_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html
Sourcespec fn get_Some_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_Some_0(&self) -> T
get_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html
Sourcespec fn is_None(&self) -> bool
👎Deprecated: is_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html
spec fn is_None(&self) -> bool
is_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html
Sourcespec fn arrow_Some_0(&self) -> T
spec fn arrow_Some_0(&self) -> T
Sourceproof fn tracked_unwrap(tracked self) -> tracked t : T
proof fn tracked_unwrap(tracked self) -> tracked t : T
self.is_Some(),t == self->0,Sourceproof fn tracked_expect(tracked self, msg: &str) -> tracked t : T
proof fn tracked_expect(tracked self, msg: &str) -> tracked t : T
self.is_Some(),t == self->0,Sourceproof fn tracked_borrow(tracked &self) -> tracked t : &T
proof fn tracked_borrow(tracked &self) -> tracked t : &T
self.is_Some(),t == self->0,Sourceproof fn tracked_take(tracked &mut self) -> tracked t : T
proof fn tracked_take(tracked &mut self) -> tracked t : T
old(self).is_Some(),t == old(self)->0,final(self).is_None(),Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.
Implementations on Foreign Types§
Source§impl<T> OptionAdditionalFns<T> for Option<T>
impl<T> OptionAdditionalFns<T> for Option<T>
Source§open spec fn is_Some(&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_Some(&self) -> bool
is_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html
{ is_variant(self, "Some") }Source§open spec fn get_Some_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_Some_0(&self) -> T
get_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html
{ get_variant_field(self, "Some", "0") }Source§open spec fn is_None(&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_None(&self) -> bool
is_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html
{ is_variant(self, "None") }Source§open spec fn arrow_Some_0(&self) -> T
open spec fn arrow_Some_0(&self) -> T
{ get_variant_field(self, "Some", "0") }Source§proof fn tracked_unwrap(tracked self) -> tracked t : T
proof fn tracked_unwrap(tracked self) -> tracked t : T
Source§proof fn tracked_expect(tracked self, msg: &str) -> tracked t : T
proof fn tracked_expect(tracked self, msg: &str) -> tracked t : T
Source§proof fn tracked_borrow(tracked &self) -> tracked t : &T
proof fn tracked_borrow(tracked &self) -> tracked t : &T
Source§proof fn tracked_take(tracked &mut self) -> tracked t : T
proof fn tracked_take(tracked &mut self) -> tracked t : T
Similar to Option::take