Skip to content
GitLab

Add lemmas `map_intersection_filter` and `map_difference_filter`.

Merged Robbert Krebbers requested to merge robbert/intersection_difference_filter into master

See also the discussion in iris!697 (diffs, comment 69805)

Edited by Robbert Krebbers