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
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: May 14 2021 at 12:18 UTC