vstd
In vstd::
invariant
vstd
::
invariant
Macro
open_local_invariant_in_proof
Copy item path
Source
macro_rules! open_local_invariant_in_proof { [$($tail:tt)*] => { ... }; }