by_cases message

Stream: new members

[Shing Tak Lam]

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]

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]

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]

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.