Skip to content

Better instance for `IntoWand` of `∀ _ : φ, P`

Robbert Krebbers requested to merge robbert/iSpecialize_forall into master

This MR makes sure that iSpecialize on ∀ _ : φ, P behaves the same as ⌜ φ ⌝ → P, which in turn was designed to behave the same as <affine> φ -∗ P. Similar to ⌜ φ ⌝ → P, affine modalities are only added in a general BI, not in an affine BI.

The old behavior was that ∀ _ : φ, P was consider equivalent to φ -∗ P, but that required P to be absorbing. That seems like a weird condition...

The tests are variants of those we have for ⌜ φ ⌝ → P.

This fixes issue #492 (closed).

Edited by Robbert Krebbers

Merge request reports