Struct ViewUpdateRemove 

pub struct ViewUpdateRemove<R: ViewRel>(pub Snapshot<R::Auth>);

Tuple Fields

0: Snapshot<R::Auth>

Trait Implementations

impl<R: ViewRel> Update<View<R>> for ViewUpdateRemove<R>

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

(open)

pearlite! {
    from.auth() != None &&
    forall<f: R::Frag>
        match from.frag().op(f) {
            Some(ff) => R::rel(from.auth(), ff),
            None => false
        } ==>
        R::rel(Some(*self.0), f)
}

fn update(self, from: View<R>, _: ()) -> View<R>

(open)

View::new_auth(*self.0)

requires

self.premise(from)

ensures

R::rel(Some(*self.0), R::Frag::unit())

fn frame_preserving(self, from: View<R>, frame: View<R>)

requires

self.premise(from)

requires

from.op(frame) != None

ensures

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

type Choice = ()