A Different `finset.fold`

Stream: Is there code for X?

[Marcus Rossel]

The definition of finset.fold is explained as follows:

fold op b f s folds the commutative associative operation op over the f-image of s,
i.e. fold (+) b f {1,2,3} = f 1 + f 2 + f 3 + b.

The consequence of this is that the types of b and f x have to match.
Is there someway to perform a fold over a finset, where b can have a different type than f x?
And e.g. the requirement could be that ...

∀ (x y : α) (b : β), op (op b (f x)) (f y) = op (op b (f y)) (f x)

[Eric Wieser]

I suspect the issue is that the typeclasses used to express the current docs#finset.fold don't exist to express what you suggest

[Eric Wieser]

(I guess this applies to docs#multiset.fold too)

[Eric Wieser]

Ah, I think you want (s.1.map f).foldr op b (docs#multiset.foldr)

[Marcus Rossel]

Ahhh that's exactly it. Thanks for always being so helpful @Eric Wieser!