Struct ViewUpdateInsert 

pub struct ViewUpdateInsert<R: ViewRel>(pub Snapshot<R::Auth>, pub Snapshot<R::Frag>);

Tuple Fields

0: Snapshot<R::Auth>

1: Snapshot<R::Frag>

Trait Implementations

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

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

(open)

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

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

(open)

View::new(Some(*self.0), *self.1)

requires

self.premise(from)

ensures

R::rel(Some(*self.0), *self.1)

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 = ()