dfinsupp vs finsupp

Stream: maths

[Yury G. Kudryashov]

Hi, I see that dfinsupp is implemented using multiset, pre_support, and quotient while finsupp is implemented using finset and support. Is there any particular reason for this difference?
I mean, before looking into the sources I expected finsupp α β = dfinsupp α (λ _, β).

[Chris Hughes]

No good reason really. I think they were just written at different times by different people with different tastes.

[Yury G. Kudryashov]

As far as I understand, dfinsupp works without some decidable_eq assumptions while finsupp doesn't (or creates noncomputable defs).

[Kenny Lau]

Yep. That's why I chose it.