Struct SumLocalUpdateR 

pub struct SumLocalUpdateR<U>(pub U);

Apply an update to the Right variant of an authority/fragment pair of Sums.

This requires either the authority or the fragment to be in the Right state (the other will be implied as they must always be in the same state).

Tuple Fields

0: U

Trait Implementations

impl<R1: RA, R2: RA, U: LocalUpdate<R2>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateR<U>

fn premise(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> bool

logic(open, inline)

match (from_auth, from_frag) {
    (Sum::Right(from_auth), Sum::Right(from_frag)) => self.0.premise(from_auth, from_frag),
    (Sum::Left(_), Sum::Left(_)) => false,
    _ => true,
}

fn update( self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>, ) -> (Sum<R1, R2>, Sum<R1, R2>)

logic(open, inline)

/* Macro-generated */

fn frame_preserving( self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>, frame: Option<Sum<R1, R2>>, )

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