Struct SumLocalUpdateL 

pub struct SumLocalUpdateL<U>(pub U);

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

(open)

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

(open)

match (from_auth, from_frag) {
    (Sum::Left(from_auth), Sum::Left(from_frag)) => {
        let (to_auth, to_frag) = self.0.update(from_auth, from_frag);
        (Sum::Left(to_auth), Sum::Left(to_frag))
    }
    _ => such_that(|_| true),
}

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

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