Struct FMapInsertLocalUpdate 

pub struct FMapInsertLocalUpdate<K, V>(pub Snapshot<K>, pub Snapshot<V>);

Tuple Fields

0: Snapshot<K>

1: Snapshot<V>

Trait Implementations

impl<K, V: RA> LocalUpdate<FMap<K, V>> for FMapInsertLocalUpdate<K, V>

fn premise(self, from_auth: FMap<K, V>, _: FMap<K, V>) -> bool

(open)

from_auth.get(*self.0) == None

fn update( self, from_auth: FMap<K, V>, from_frag: FMap<K, V>, ) -> (FMap<K, V>, FMap<K, V>)

(open)

(from_auth.insert(*self.0, *self.1), from_frag.insert(*self.0, *self.1))

fn frame_preserving( self, from_auth: FMap<K, V>, from_frag: FMap<K, V>, frame: Option<FMap<K, V>>, )

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