Skip to content

GitLab

I
Iris
Merged
Opened by Robbert@robbertkrebbersMaintainer

Generalize `iPureIntro` to support non-empty spatial contexts with just affine hypotheses.

This MR makes it possible to introduce pure facts, even if the spatial context is non-empty, as long as all hypotheses in it are affine (which is trivially true when working in an affine BI).

We already had this behavior for iEmpIntro, so it makes sense to have it for iPureIntro too.

As part of this MR, I had to change the modes of the FromPure class:

Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
  from_pure : <affine>?a ⌜φ⌝ ⊢ P.
Hint Mode FromPure + - ! - : typeclass_instances.

The a argument is now an output, rather than an input. It tells one whether the spatial context needs to be affine or not.