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>
4 lines
510 B
Text
4 lines
510 B
Text
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`.
|