Function vstd::pcm_lib::copy_duplicable_part

source · 
pub proof fn copy_duplicable_part<P: PCM>(tracked 
    r: &Resource<P>,
    new_value: P
) -> tracked out : Resource<P>
Expand description
requires
r.value() == P::op(r.value(), new_value),
ensures
out.loc() == r.loc(),
out.value() == new_value,

Produces a new resource with value new_value given an immutable reference to a resource r whose value has a duplicable part new_value. More precisely, produces a resource with value new_value given that r.value() == P::op(r.value(), new_value).