Trait vstd::std_specs::option::OptionAdditionalFns
source · pub trait OptionAdditionalFns<T>: Sized {
// Required methods
fn is_Some(&self) -> bool;
fn get_Some_0(&self) -> T;
fn is_None(&self) -> bool;
fn arrow_Some_0(&self) -> T;
fn arrow_0(&self) -> T;
fn tracked_unwrap(self) -> T;
fn tracked_borrow(&self) -> &T;
}Required Methods§
sourcespec fn get_Some_0(&self) -> T
spec fn get_Some_0(&self) -> T
sourcespec fn arrow_Some_0(&self) -> T
spec fn arrow_Some_0(&self) -> T
sourceproof fn tracked_unwrap(tracked self) -> tracked T
proof fn tracked_unwrap(tracked self) -> tracked T
sourceproof fn tracked_borrow(tracked &self) -> &T
proof fn tracked_borrow(tracked &self) -> &T
Object Safety§
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 get_Some_0(&self) -> T
open spec fn get_Some_0(&self) -> T
{ get_variant_field(self, "Some", "0") }source§open spec fn arrow_Some_0(&self) -> T
open spec fn arrow_Some_0(&self) -> T
{ get_variant_field(self, "Some", "0") }