Skip to content

Simplify definition of invariant model.

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.

Merge request reports