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§

source

spec fn is_Some(&self) -> bool

source

spec fn get_Some_0(&self) -> T

source

spec fn is_None(&self) -> bool

source

spec fn arrow_Some_0(&self) -> T

source

spec fn arrow_0(&self) -> T

source

proof fn tracked_unwrap(tracked self) -> tracked t : T

requires
self.is_Some(),
ensures
t == self.get_Some_0(),
source

proof fn tracked_borrow(tracked &self) -> tracked t : &T

requires
self.is_Some(),
ensures
t == self.get_Some_0(),

Object Safety§

This trait is not object safe.

Implementations on Foreign Types§

source§

impl<T> OptionAdditionalFns<T> for Option<T>

source§

open spec fn is_Some(&self) -> bool

{ is_variant(self, "Some") }
source§

open spec fn get_Some_0(&self) -> T

{ get_variant_field(self, "Some", "0") }
source§

open spec fn is_None(&self) -> bool

{ is_variant(self, "None") }
source§

open spec fn arrow_Some_0(&self) -> T

{ get_variant_field(self, "Some", "0") }
source§

open spec fn arrow_0(&self) -> T

{ get_variant_field(self, "Some", "0") }
source§

proof fn tracked_unwrap(tracked self) -> tracked t : T

source§

proof fn tracked_borrow(tracked &self) -> tracked t : &T

Implementors§