Zulip Chat Archive

Stream: general

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: Dec 20 2023 at 11:08 UTC