Zulip Chat Archive
Stream: mathlib4
Topic: Order.PFilter
Violeta Hernández (Dec 02 2024 at 09:49):
Isn't docs#Filter a special case of docs#Order.PFilter ? Is there any reason to have both separately?
Patrick Massot (Dec 02 2024 at 10:18):
Yes, this has been discussed many times. You can search on Zulip if you are curious.
Anatole Dedecker (Dec 02 2024 at 10:30):
That said it would be nice for docs#Order.Ideal and docs#Order.PFilter to get a bit more love, these are useful notions (and we don't have a set-specialized docs#Order.Ideal).
Yaël Dillies (Dec 02 2024 at 11:39):
It's one of the many refactors on my TODO list :sad:
Last updated: May 02 2025 at 03:31 UTC