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
iRight was needed.
I wonder if Iris could still benefit from such rules by adding a marker in the syntax for
iFrame "!H", which applies the more reckless disjunction framing rules. The same could be applied for specialization patterns with something like
What do you think?