Trait vstd::std_specs::option::OptionAdditionalFns
source · 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_borrow(tracked &self) -> tracked t : &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 : T
proof fn tracked_unwrap(tracked self) -> tracked t : T
sourceproof fn tracked_borrow(tracked &self) -> tracked t : &T
proof fn tracked_borrow(tracked &self) -> tracked t : &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") }