dedup and eraseDup

Stream: mathlib4

[Wrenna Robson]

Why does Batteries have List.eraseDup and Mathlib have List.dedup, which are virtually identical, but as far as I can tell we don't have a theorem even linking the two?

[Wrenna Robson]

We also have List.eraseDups which... seems to do the same thing as eraseDup?

[Wrenna Robson]

Indeed I think List.pwFilter and List.eraseDupsBy might be virtually the same as well...

[Ruben Van de Velde]

One in core, one in batteries, one in mathlib. Sounds sensible, right? :sweat_smile:

[Wrenna Robson]

I take the perhaps controversial view that we should only have one of these ;)

[Ruben Van de Velde]

Two of them claim to be defined as pwFilter (≠), but one claims the last is kept and one that the first is kept

[Ruben Van de Velde]

Also core and batteries use BEq and mathlib DecidableEq

[Wrenna Robson]

Yes, although pwFilter uses DecidableEq again in Batteries.

[Ruben Van de Velde]

I wonder if the change to make BEq and DecidableEq play nicer together ever landed

[Wrenna Robson]

I think it does seem to...

[Eric Wieser]

I thought it didn't, and we had to change Decidable to be a subtype of Bool for that to work

[Wrenna Robson]

Looking at the definition of pwFilter, I think in practice it will drop the first element that duplicates a later element in the list.

[Ruben Van de Velde]

Anyway, I agree at least the one in batteries should be deprecated

[Ruben Van de Velde]

https://github.com/leanprover/lean4/pull/8309 ?