Skip to content

Finite map composition

Dorian Lesbre requested to merge dlesbre/stdpp:dorian/map_compose into master
  • Add a map_compose operator for finite map composition
  • Add notation m ∘ₘ n for map_compose m n
  • Add various lemmas to manipulate map composition

This is arguably a niche operator we might not want to include. If you think that is the case feel free to close without merging.

I'm submitting in case someone else would have a use for it, since this is now fairly complete (although it could use some compatibility lemmas with insert).

Merge request reports