Skip to content

Add `gmultiset_map` and associated lemmas

Marijn van Wezel requested to merge marijnvanwezel/stdpp:marijn/gmultiset_map into master

This merge request adds a definition for mapping over a gmultiset, gmultiset_map, similar to set_map for (regular) finite sets.

I struggled with finding a correct location for the definition and associated lemmas in gmultiset.v. I am open to any suggestions to improve the placement.

Edited by Marijn van Wezel

Merge request reports