Trait OptionExtraFns 

pub trait OptionExtraFns<T> {
    // Required methods
    spec fn tracked_borrow_mut_requires(self) -> bool;
    spec fn tracked_borrow_mut_ensures(self, value: T) -> bool;
    proof fn tracked_borrow_mut(tracked &mut self) -> tracked value : &mut T;
}

Required Methods

spec fn tracked_borrow_mut_requires(self) -> bool

spec fn tracked_borrow_mut_ensures(self, value: T) -> bool

proof fn tracked_borrow_mut(tracked &mut self) -> tracked value : &mut T

requires

self.tracked_borrow_mut_requires(),

ensures

old(self).tracked_borrow_mut_ensures(*value),

final(self).tracked_borrow_mut_ensures(*final(value)),

Implementations on Foreign Types

impl<T> OptionExtraFns<T> for Option<T>

open spec fn tracked_borrow_mut_requires(self) -> bool

{ self is Some }

open spec fn tracked_borrow_mut_ensures(self, value: T) -> bool

{ self is Some && self->0 == value }

proof fn tracked_borrow_mut(tracked &mut self) -> tracked &mut T

Implementors