Zulip Chat Archive

Stream: general

Topic: set_semiring

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 up/down for set_semiring. If you have better suggestions, feel free to change them.

Last updated: Dec 20 2023 at 11:08 UTC