Skip to content

More general instance for framing under `<affine>`

Robbert Krebbers requested to merge robbert/iFrame_affine into master

Allow framing below an modality if the hypothesis that is framed is affine. (Previously, framing below was only possible if the hypothesis that is framed resides in the intuitionistic context.)

This is part (1) of !450 (closed). See !521 (merged) for a discussion why we don't want the rest of that MR.

Merge request reports