constructor

Stream: lean4

[Antoine Chambert-Loir]

Today, a student typed constructor when he had to prove an Or formula, and Lean answered by picking up the left branch of the or, without any hint that the other branch was possible.
Is this the expected behaviour for the constructor tactic?

[Damiano Testa]

Unfortunately yes, there is an issue about it: let me look it up!

[Damiano Testa]

lean4#3129

[Damiano Testa]

(as you can see from the issue, I was bitten by this for Decidable.)

[Kyle Miller]

Here's the previous thread about this, linked to from the issue.