pub proof fn extract<P: PCM>(tracked r: &mut Resource<P>) -> tracked other : Resource<P>Expand description
ensures
other.loc() == r.loc() == old(r).loc(),r.value() == P::unit(),other.value() == old(r).value(),Extracts the resource from r, leaving r empty (i.e., having
value P::unit) and returning a new resource holding the previous
value of r.