Skip to content

Remove `map` infix in lemmas about `dom` and `filter`.

Robbert Krebbers requested to merge robbert/dom_filter into master

The combination of dom and filter only makes sense for maps, so the map infix is useless. Other similar lemmas do not have such an infix either, so it's also inconsistent.

Rename dom_map filter → dom_filter, dom_map_filter_L → dom_filter_L, and dom_map_filter_subseteq → dom_filter_subseteq.

This was pointed out by @atrieu in !175 (comment 53746)

Edited by Robbert Krebbers

Merge request reports