Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
Due to the new semantic invariants (!319) we no longer need to close the model (i.e. `inv_def`) to be contractive, the semantic invariant definition (i.e. `inv`) is already contractive.
Robbert Krebbers authoredDue to the new semantic invariants (!319) we no longer need to close the model (i.e. `inv_def`) to be contractive, the semantic invariant definition (i.e. `inv`) is already contractive.
