• Robbert Krebbers's avatar
    Simplify definition of invariant model. · 0b860f2a
    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.
    0b860f2a
invariants.v 6.54 KB