Skip to content
GitLab

Simplify definition of invariant model.

Merged Robbert Krebbers requested to merge robbert/invariants into master

Due to the new semantic invariants (!319 (merged)) 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.