`iFrame` peforms some surprising modality cleanup
Framing <affine> P
on goal <affine> <affine> (P ∗ Q)
produces the result <affine> Q
. I think that is rather srprising and would have expected <affine> <affine> Q
. It seems like as it traverses the term, iFrame
is a bit too quick to apply the MakeAffine
class even when there was a literal affinely modality before that should IMO just be preserved.
For <absorb>
and <pers>
, iFrame
just fails in the same situation. The same is true for □
, but when one has P
in the intuitionistic context, then one can frame into goal □ □ (P ∗ Q)
and once !842 (closed) lands that will produce □ Q
.