Skip to content

Strengthen validy of fragment of view camera

Robbert Krebbers requested to merge robbert/view_frag_valid into master

That is, strengthen ✓{n} (◯V b) into ∃ a, rel n a b.

This was discussed in !543 (comment 58219)

Note that as a consequence of this change, ✓ (◯ b) is no longer definitionally equal to ✓ b.

Edited by Robbert Krebbers

Merge request reports