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