Framing in Disjunctions
@haidang and I used to have two Instances for Frame that would let us frame out things from only one side of a disjunction. We currently do not have that instance anymore – apparently, it got lost somehow – but we miss it. I do realize that such an instance potentially leads to unsolvable goals more often than any of the existing framing instances. So this should probably not be the default behavior of iFrame
. Nonetheless, the functionality was extremely convenient in some places. Often, disjunctive goals could easily be closed by framing out a bunch of resources and closing the goal with a by
prefix or a separate done
. No iLeft
or iRight
was needed.
I wonder if Iris could still benefit from such rules by adding a marker in the syntax for iFrame
, e.g. iFrame "!H"
, which applies the more reckless disjunction framing rules. The same could be applied for specialization patterns with something like $!H
.
What do you think?