Struct SumUpdateL 

pub struct SumUpdateL<U>(pub U);

Apply an update to the left side of a Sum.

This requires the resource to be in the Left state.

Example

use creusot_std::{
    ghost::resource::Resource,
    logic::ra::{
        excl::{Excl, ExclUpdate},
        sum::{Sum, SumUpdateL},
    },
    prelude::*,
};

let mut res: Ghost<Resource<Sum<Excl<Int>, Excl<()>>>> =
    Resource::alloc(snapshot!(Sum::Left(Excl(1))));
ghost! { res.update(SumUpdateL(ExclUpdate(snapshot!(2)))) };
proof_assert!(res@ == Sum::Left(Excl(2)));

Tuple Fields

0: U

Trait Implementations

impl<R1: RA, R2: RA, U: Update<R1>> Update<Sum<R1, R2>> for SumUpdateL<U>

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

logic(open, inline)

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

fn update(self, from: Sum<R1, R2>, ch: U::Choice) -> Sum<R1, R2>

logic(open, inline)

match from {
    Sum::Left(from) => Sum::Left(self.0.update(from, ch)),
    x => x, /* Dummy */
}

requires

self.premise(from)

fn frame_preserving(self, from: Sum<R1, R2>, frame: Sum<R1, R2>) -> U::Choice

logic

requires

self.premise(from)

requires

from.op(frame) != None

ensures

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

type Choice = <U as Update<R1>>::Choice

If the update is non-deterministic, it will pick a choice of this type for the update.