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".
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