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>
2 lines
261 B
Text
2 lines
261 B
Text
247.lean:8:11-8:33: error: Cannot lift nested action `← uinfoldDefinition? b` 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`.
|