deduplicating List.dedup and List.eraseDups

Stream: general

[Eric Wieser]

I noticed that we have both docs#List.dedup (DecidableEq) and docs#List.eraseDups (BEq). Should we deduplicate these, or erase the duplication?

[Eric Wieser]

(If we drop dedup, then we should rename some downstream definitions too)

[Ruben Van de Velde]

Do we need to solve https://github.com/leanprover/lean4/pull/2038 first?

[Eric Wieser]

Quite possibly

[Eric Wieser]

I think there's a lot of API tension between functions taking Bool relations and functions taking Prop relations

[Eric Wieser]

(for instance, docs#List.pwFilter explains that it can be used to implement deduplication, but this function takes a true relation, and so is analogous todedup not eraseDup)

[Kim Morrison]

Waiting on lean4#2038 doesn't seem like a productive choice.