Additional lemmas about map_imap

Some lemmas that were useful to me in a development.

Thanks for the MR. Modulo small comments about syntax and naming, this seems fine.

added 1 commit

• a76c295a - Apply Robbert's suggestions

Compare with previous version

resolved all threads

Applied all suggestions, however, for the naming part, I initially followed the naming used in dom_map_filter, so this may also need to be renamed to dom_filter for consistency ?

Applied all suggestions

Thanks. LGTM.

However, for the naming part, I initially followed the naming used in dom_map_filter, so this may also need to be renamed to dom_filter for consistency ?

Yes, I think so. Let me fix that in a separate MR.

merged

mentioned in commit ef460edd

mentioned in commit 5710f90e

mentioned in merge request !176 (merged)