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
vstd
::
invariant
Function
create_open_invariant_credit
Copy item path
Settings
Help
Summary
Source
pub
exec
fn create_open_invariant_credit() ->
Tracked
<OpenInvariantCredit>
Expand description