Strange error message

Stream: general

[Patrick Massot]

code generation failed, VM does not have code for 'classical.choice' seems to be Lean trying to tell me to stop considering examples and go back to work

[Mario Carneiro]

you can't compute the noncomputable

[Patrick Massot]

Yes I understand

[Patrick Massot]

funny part is I thought I wasn't using choice

[Patrick Massot]

Actually I used a small #eval to test something in the middle of a file I was working on. Of course this file begins the mathematical preamble, including local attribute [instance] classical.prop_decidable

[Patrick Massot]

Removing that line makes eval to succeed

[Patrick Massot]

So the line can prevent computing even things which are actually computable. That's nice defense against constructivism

[Chris Hughes]

You can use local attribute [instance, priority 0] classical.prop_decidable to preserve computability when possible.