Skip to content

Add lemmas `map_intersection_filter` and `map_difference_filter`.

Robbert Krebbersrequested to merge
robbert/intersection_difference_filter into master

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

Edited by Robbert Krebbers

Merge request reports