vstd::pcm_lib

Function 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.