vstd::modes

Function 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),