Function vstd::pcm_lib::incorporate

source · 
pub proof fn incorporate<P: PCM>(tracked r1: &mut Resource<P>, tracked r2: Resource<P>)
Expand description
requires
old(r1).loc() == r2.loc(),
ensures
r1.loc() == old(r1).loc(),
r1.value() == P::op(old(r1).value(), r2.value()),

Incorporates the resources of r2 into r1, consuming r2.