Struct AuthUpdate 

pub struct AuthUpdate<U>(pub U);

Tuple Fields

0: U

Trait Implementations

impl<R: UnitRA, U: LocalUpdate<R>> Update<View<AuthViewRel<R>>> for AuthUpdate<U>

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

(open)

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

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

(open)

let from_auth = from.auth().unwrap_logic();
let (auth, frag) = self.0.update(from_auth, from.frag());
self.0.frame_preserving(from_auth, from.frag(), from_auth.factor(from.frag()));
Auth::new(Some(auth), frag)

requires

self.premise(from)

ensures

let (auth, frag) = self.0.update(from.auth().unwrap_logic(), from.frag());
AuthViewRel::rel(Some(auth), frag)

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

requires

self.premise(from)

requires

from.op(frame) != None

ensures

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

type Choice = ()