Zulip Chat Archive

Stream: mathlib4

Topic: Where should List.mem_eraseDup and List.mem_eraseDups l...

Notification Bot (Dec 28 2025 at 22:48):

This topic was moved to #batteries > Where should List.mem_eraseDup and List.mem_eraseDups l... by Yury G. Kudryashov.

Last updated: Feb 28 2026 at 14:05 UTC