Skip to content

Make `iFrame` fail if more work remains

Robbert Krebbers requested to merge robbert/iFrame_fail_more_work into master

This addresses #582

Simple example:

Lemma foo `{BiAffine PROP} (P Q : PROP) : P -∗ Q -∗ P.
Proof.
  iIntros "HP HQ".
  Fail iFrame "HP HQ". (* Framing [HP] turns the goal into [True], but more work
  (framing [HQ]) remains, hence [iFrame] fails. *)
  Fail iFrame "HQ HP". (* Fails because [HQ] cannot be framed in the first place. *)
Abort.
Edited by Robbert Krebbers

Merge request reports