Struct SumLocalUpdateL 

pub struct SumLocalUpdateL<U>(pub U);

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

This requires either the authority or the fragment to be in the Left 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<R1>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateL<U>

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

logic(open, inline)

match (from_auth, from_frag) {
    (Sum::Left(from_auth), Sum::Left(from_frag)) => self.0.premise(from_auth, from_frag),
    (Sum::Right(_), Sum::Right(_)) => 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))