Topic: order on bool
Rob Lewis (Jun 15 2020 at 16:37):
See the discussion here: https://github.com/leanprover-community/mathlib/pull/2637#discussion_r440039075
Mario questions putting a global order instance on
bool. It doesn't matter much to me -- I only need it locally -- but I don't really see the harm in the global instance. Am I missing something?
(There's a stronger lattice structure on
bool too, of course, but I'm not interested in setting it up for this PR.)
Floris van Doorn (Jun 15 2020 at 18:23):
I don't see the harm either.
Bryan Gin-ge Chen (Jun 15 2020 at 20:22):
@Mario Carneiro is this the only thing holding up this PR?
Last updated: Aug 03 2023 at 10:10 UTC