-
Robbert Krebbers authored
- It can now also frame under later. - Better treatment of evars, it now won't end up in loops whenever the goal involves sub-formulas ?P and it trying to apply all framing rules eagerly. - It no longer delta expands while framing. - Better clean up of True sub-formulas after a successful frame. For example, framing "P" in "▷ ▷ P ★ Q" yields just "Q" instead of "▷ True ★ Q" or so.
43d45c6bRobbert Krebbers authored- It can now also frame under later. - Better treatment of evars, it now won't end up in loops whenever the goal involves sub-formulas ?P and it trying to apply all framing rules eagerly. - It no longer delta expands while framing. - Better clean up of True sub-formulas after a successful frame. For example, framing "P" in "▷ ▷ P ★ Q" yields just "Q" instead of "▷ True ★ Q" or so.
Loading