vstd
In vstd::
invariant
Macros
open_atomic_invariant
open_atomic_invariant_in_proof
open_local_invariant
open_local_invariant_in_proof
Structs
AtomicInvariant
LocalInvariant
Traits
InvariantPredicate
Functions
create_open_invariant_credit
?
Settings
Macro
vstd
::
invariant
::
open_atomic_invariant_in_proof
Copy item path
source
·
[
−
]
macro_rules!
open_atomic_invariant_in_proof { [$(
$tail
:tt)
*
] => { ... }; }