Skip to main content

Module resource_invariant

vstd_extra

Module resource_invariant 

Source

Structs§

TrivialResourceInvariant
A resource invariant that imposes no condition on the value.

Traits§

ResourceInvariant
An invariant that relates a value to a tracked resource with a constant.
SimpleResourceInvariant
A resource invariant that does not need a constant.
ValueInvariant
A resource invariant that only considers the value.