mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
40e8f4c5fb
This PR turns on the new `do` elaborator in Init, Lean, Std, Lake and the testsuite. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
5 lines
510 B
Plaintext
5 lines
510 B
Plaintext
liftOverLeft.lean:4:11-4:18: error: Cannot lift nested action `← x.get` over a binder.
|
|
This error usually happens when you are trying to lift a method nested in a `fun`, `let`, or `match`-alternative, and it can often be fixed by adding a missing `do`.
|
|
liftOverLeft.lean:9:11-9:18: error: Cannot lift nested action `← x.get` over a binder.
|
|
This error usually happens when you are trying to lift a method nested in a `fun`, `let`, or `match`-alternative, and it can often be fixed by adding a missing `do`.
|