vstd::std_specs::option

Trait 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;
    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§

Source

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
Source

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
Source

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
Source

spec fn arrow_Some_0(&self) -> T

Source

spec fn arrow_0(&self) -> T

Source

spec fn tracked_is_some(&self) -> bool

Auxilliary spec function for the spec of tracked_unwrap, tracked_borrow, and tracked_take.

Source

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

requires
self.tracked_is_some(),
ensures
t == self->0,
Source

proof fn tracked_expect(tracked self, msg: &str) -> tracked t : T

requires
self.tracked_is_some(),
ensures
t == self->0,
Source

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

requires
self.tracked_is_some(),
ensures
t == self->0,
Source

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

requires
old(self).tracked_is_some(),
ensures
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>

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
{ 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
{ 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
{ 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§

open spec fn tracked_is_some(&self) -> bool

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

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

Source§

proof fn tracked_expect(tracked self, msg: &str) -> tracked t : T

Source§

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

Source§

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

Similar to Option::take

Implementors§