Yaël Dillies (Mar 15 2022 at 09:53):
Just noting that the reason docs#set.up_le_up can't be
simp is that the
≤ on the LHS is
set.has_le, not the defeq
set.set_semiring.has_le. I don't know how to fix this without writing it out entirely or giving up on the
derive partial_order (which could be strengthened to
derive complete_boolean_algebra btw).
Let me also repeat that docs#set.up and docs#set.set_semiring.down are terrible names. :grinning:
cc @Damiano Testa
Gabriel Ebner (Mar 15 2022 at 10:00):
BTW, it's docs#set.set_semiring.down
Floris van Doorn (Mar 15 2022 at 10:30):
I might be responsible for the names
set_semiring. If you have better suggestions, feel free to change them.
Last updated: Aug 03 2023 at 10:10 UTC