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>
3 lines
204 B
Text
3 lines
204 B
Text
doLetLoop.lean:6:0: error: unexpected end of input
|
|
doLetLoop.lean:5:2-5:8: error: unexpected `do` element syntax
|
|
failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)
|