Extend ElimModal with Boolean flags to specify whether it operates on the… (!129) · Merge requests · Iris / Iris

Extend ElimModal with Boolean flags to specify whether it operates on the persistent/spatial context:

Class ElimModal {PROP : bi} (φ : Prop) (p p' : bool) (P P' : PROP) (Q Q' : PROP) :=
  elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q.

This provides a preparation for #167.

Edited Mar 15, 2018 by Robbert Krebbers

Extend ElimModal with Boolean flags to specify whether it operates on the…