Struct OptionUpdate 

pub struct OptionUpdate<U>(pub U);

Tuple Fields

0: U

Trait Implementations

impl<R: RA, U: Update<R>> Update<Option<R>> for OptionUpdate<U>

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

(open)

match from {
    Some(from) => self.0.premise(from),
    None => false,
}

fn update(self, from: Option<R>, ch: U::Choice) -> Option<R>

(open)

match from {
    Some(from) => Some(self.0.update(from, ch)),
    None => None, /* Dummy */
}

requires

self.premise(from)

fn frame_preserving(self, from: Option<R>, frame: Option<R>) -> U::Choice

requires

self.premise(from)

requires

from.op(frame) != None

ensures

self.update(from, result).op(frame) != None

type Choice = <U as Update<R>>::Choice