Struct OptionLocalUpdate 

pub struct OptionLocalUpdate<U>(pub U);

Tuple Fields

0: U

Trait Implementations

impl<R: RA, U: LocalUpdate<R>> LocalUpdate<Option<R>> for OptionLocalUpdate<U>

fn premise(self, from_auth: Option<R>, from_frag: Option<R>) -> bool

(open, inline)

match (from_auth, from_frag) {
    (Some(from_auth), Some(from_frag)) => self.0.premise(from_auth, from_frag),
    _ => false,
}

fn update( self, from_auth: Option<R>, from_frag: Option<R>, ) -> (Option<R>, Option<R>)

(open, inline)

match (from_auth, from_frag) {
    (Some(from_auth), Some(from_frag)) => {
        let (to_auth, to_frag) = self.0.update(from_auth, from_frag);
        (Some(to_auth), Some(to_frag))
    }
    _ => (None, None), // Dummy
}

fn frame_preserving( self, from_auth: Option<R>, from_frag: Option<R>, frame: Option<Option<R>>, )

requires

self.premise(from_auth, from_frag)

requires

Some(from_frag).op(frame) == Some(Some(from_auth))

ensures

let (to_auth, to_frag) = self.update(from_auth, from_frag);
Some(to_frag).op(frame) == Some(Some(to_auth))