Function vstd::pcm_lib::split_mut

source ·

pub proof fn split_mut<P: PCM>(tracked r: &mut Resource<P>, left: P, right: P) -> tracked other : Resource<P>

Expand description

requires

old(r).value() == P::op(left, right),

ensures

r.loc() == other.loc() == old(r).loc(),

r.value() == left,

other.value() == right,

Splits the value of r into left and right. At the end, r ends up with left as its value and the function returns a new resource with value right.