Function vstd::modes::tracked_swap

source · 
pub proof fn tracked_swap<V>(tracked a: &mut V, tracked b: &mut V)
Expand description
ensures
a == old(b),
b == old(a),