Struct CancelLocalUpdateUnit 

pub struct CancelLocalUpdateUnit;

Remove (cancel) a fragment from an authority, setting the fragment to unit.

This requires the fragment to remove to be cancelable.

Trait Implementations

impl<R: UnitRA> LocalUpdate<R> for CancelLocalUpdateUnit

fn premise(self, _: R, from_frag: R) -> bool

logic(open)

from_frag.cancelable()

fn update(self, from_auth: R, from_frag: R) -> (R, R)

logic(open)

from_auth.factor(from_frag).unwrap_logic(), R::unit()

fn frame_preserving(self, from_auth: R, from_frag: R, frame: Option<R>)

logic

requires

self.premise(from_auth, from_frag)

requires

Some(from_frag).op(frame) == Some(Some(from_auth))

ensures

let (to_auth, to_frag) = self.update(from_auth, from_frag);
Some(to_frag).op(frame) == Some(Some(to_auth))