Function vstd::storage_protocol::guards

source · 
pub open spec fn guards<K, V, P: Protocol<K, V>>(p: P, b: Map<K, V>) -> bool
Expand description
{ forall |q: P, t: Map<K, V>| P::rel(P::op(p, q), t) ==> b.submap_of(t) }