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