vstd
In vstd::
modes
vstd
::
modes
Function
tracked_swap
Copy item path
Source
pub
proof
fn tracked_swap<V>(
tracked
a:
&mut V
,
tracked
b:
&mut V
)
Expand description
ensures
a == old(b),
b == old(a),