vstd::pcm_lib

Function duplicate

Source 
pub proof fn duplicate<P: PCM>(tracked r: &Resource<P>) -> tracked other : Resource<P>
Expand description
requires
P::op(r.value(), r.value()) == r.value(),
ensures
other.loc() == r.loc(),
other.value() == r.value(),

Duplicates r, returning an identical resource. The value of r must be duplicable, i.e., r.value() must be equal to P::op(r.value(), r.value()).