Skip to content

GitLab

Let `iRevert` of a pure hypotheses generate a wand instead of implication.

Merged Robbert Krebbers requested to merge robbert/iRevert_pure into master

Because implications are strange and wands are nicer.

This matches with our general consensus to prefer wand/star over implication/conjunction.

In case the BI is not affine, the wand is weaker than the implication, so we add an affine modality.

Edited by Robbert Krebbers