Traversable functor for finset

Stream: maths

[Yaël Dillies]

Might anyone more CS-y than me tell me whether I got finset.traverse right in #10980? There are some lemmas I can't prove at the end.

[Kyle Miller]

For what it's worth, docs#finset.bUnion is meant to be the bind for monad finset. (It used to be called finset.bind, too.)

[Kyle Miller]

You can see it's defined from docs#multiset.bind in a similar way to how you defined finset.traverse from docs#multiset.traverse