Topic: dfinsupp vs finsupp
Yury G. Kudryashov (Oct 06 2019 at 16:47):
Hi, I see that
dfinsupp is implemented using
finsupp is implemented using
support. Is there any particular reason for this difference?
I mean, before looking into the sources I expected
finsupp α β = dfinsupp α (λ _, β).
Chris Hughes (Oct 06 2019 at 17:46):
No good reason really. I think they were just written at different times by different people with different tastes.
Yury G. Kudryashov (Oct 06 2019 at 19:55):
As far as I understand,
dfinsupp works without some
decidable_eq assumptions while
finsupp doesn't (or creates noncomputable
Kenny Lau (Oct 06 2019 at 21:22):
Yep. That's why I chose it.
Last updated: May 12 2021 at 07:17 UTC