Zulip Chat Archive

Stream: new members

Topic: by_cases message

Shing Tak Lam (Feb 25 2020 at 09:25):

I'm not sure if I'm missing something or if there is a mistake in the description for by_cases.

It says

To ensure that all propositions are decidable via classical reasoning, use  `local attribute classical.prop_decidable [instance]`.

But that line doesn't work. Looking through TPIL, I found local attribute [instance] prop_decidable which does work. Is the description a mistake or have I just missed something?

Kevin Buzzard (Feb 25 2020 at 09:28):

That's out of date now. I should think open_locale classical will do the trick (but don't put it directly after an import command because of a bug in Lean 3)

Kevin Buzzard (Feb 25 2020 at 09:29):

But you're right that local attribute classical.prop_decidable [instance] doesn't seem to work. It's in core so until a few weeks ago was impossible to change.

Gabriel Ebner (Feb 25 2020 at 10:57):

The error message is fixed now in core Lean, and will be part of the next Lean release. But yeah, please use open_locale classical instead of you're in mathlib.

Last updated: Dec 20 2023 at 11:08 UTC