Struct ViewUpdate 

pub struct ViewUpdate<R: ViewRel, Choice>(pub Snapshot<Mapping<Choice, (R::Auth, R::Frag)>>);

Apply an update to a View, that changes both the authority and the fragment part, non-deterministically.

Tuple Fields

0: Snapshot<Mapping<Choice, (R::Auth, R::Frag)>>

Trait Implementations

impl<R: ViewRel, Choice> Update<View<R>> for ViewUpdate<R, Choice>

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

logic(open, inline)

/* Macro-generated */

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

logic(open, inline)

View::new(Some(self.0[ch].0), self.0[ch].1)

requires

self.premise(from)

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

logic

requires

self.premise(from)

requires

from.op(frame) != None

ensures

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

type Choice = Choice

If the update is non-deterministic, it will pick a choice of this type for the update.