Function vstd::pcm_lib::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()).