Rename `map_filter_lookup` → `map_lookup_filter`.
Passed
Robbert Krebbers
created pipeline for commit
7b9445c3
, finished
Related merge request !506 to merge robbert/map_lookup_filter
5 minutes 37 seconds, queued for 2 seconds