pub proof fn update_mut<P: PCM>(tracked r: &mut Resource<P>, new_value: P)Expand description
requires
frame_preserving_update(old(r).value(), new_value),r.loc() == old(r).loc(),r.value() == new_value,Updates r to have new value new_value. This must be a
frame-preserving update. That is, new_value must be compatible
with all frames old(r).value() was compatible with.