Skip to content

Remove `pure_forall_2` from BI interface + BI notation for `¬`

Robbert Krebbers requested to merge robbert/bi_pure_forall into master

This is the non-controversial part of !496 (closed)

The clProp logic does not enjoy the BI law (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝. Therefore, I have removed this law from the BI interface, and factored it into a type class BiPureForall. This follows the same pattern as we use for other properties that do not hold for all BIs.

This is a breaking change for developments that define their own BI instances, but I think the only one out there is Iron.

Edited by Robbert Krebbers

Merge request reports