List.eraseDups.Nodup

Stream: Is there code for X?

[Snir Broshi]

docs#List.eraseDups has almost no API, but I expected a Nodup theorem to at least exist.
Does anyone care about this def, or is there a replacement in Mathlib with more API?

[Ruben Van de Velde]

We recently had a discussion about this and... eraseDup? Is this the one that's kept?

[Robin Arnez]

docs#List.dedup has more API

[Snir Broshi]

Nice! Should we try to upstream some? What was the previous discussion?

[Robin Arnez]

#batteries > Where should List.mem_eraseDup and List.mem_eraseDups l...