Skip to content

Make `iFrame` "less" smart w.r.t. clean up of modalities.

Robbert Krebbers requested to merge robbert/more_dumb_iFrame into master

Previously, iFrame would "cleanup" <affine> and if the result after framing is affine and intuitionistic, respectively. This behavior was inconsistent, since similar "cleanup" was not performed for <absorbing> and <persistent>. This MR thus removes this "cleanup" of modalities. It now consistently removes the modalities <affine>, <absorbing>, <persistent> and only if the result after framing is True or emp.

Since iFrame is already very complicated, and since its performance is sometimes suboptimal in bigger developments, @jung and I believed doing fewer "smart" things is better than the alternative, namely performing doing sophisticated "cleanup" for all modalities, which is presented in !450 (closed)

Edited by Robbert Krebbers

Merge request reports