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;
spec fn tracked_is_some(&self) -> bool;
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
-> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.htmlSourcespec fn get_Some_0(&self) -> T
👎Deprecated: is_Variant is deprecated - use -> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html
spec fn get_Some_0(&self) -> T
-> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.htmlSourcespec 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
-> or matches instead: https://verus-lang.github.io/verus/guide/datatypes_enum.htmlSourcespec fn arrow_Some_0(&self) -> T
spec fn arrow_Some_0(&self) -> T
Sourcespec fn tracked_is_some(&self) -> bool
spec fn tracked_is_some(&self) -> bool
Auxilliary spec function for the spec of tracked_unwrap, tracked_borrow, and tracked_take.
Sourceproof fn tracked_unwrap(tracked self) -> tracked t : T
proof fn tracked_unwrap(tracked self) -> tracked t : T
requires
self.tracked_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
requires
self.tracked_is_some(),t == self->0,Sourceproof fn tracked_borrow(tracked &self) -> tracked t : &T
proof fn tracked_borrow(tracked &self) -> tracked t : &T
requires
self.tracked_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
requires
old(self).tracked_is_some(),t == old(self)->0,!self.tracked_is_some(),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
-> 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: is_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
-> 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
-> 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§open spec fn tracked_is_some(&self) -> bool
open spec fn tracked_is_some(&self) -> bool
{ is_variant(self, "Some") }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