set_semiring

Stream: general

[Yaël Dillies]

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]

BTW, it's docs#set.set_semiring.down

[Floris van Doorn]

I might be responsible for the names up/down for set_semiring. If you have better suggestions, feel free to change them.