Zulip Chat Archive
Stream: mathlib4
Topic: Should `Set.inclusion` be an `abbrev`?
Matthew Ballard (Aug 13 2024 at 20:18):
I don't see any situation where we don't want to reduce docs#Set.inclusion off the top of my head
Matthew Ballard (Aug 14 2024 at 16:50):
#15812 -- seems like a clear win
Last updated: May 02 2025 at 03:31 UTC