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>
16 lines
276 B
Text
16 lines
276 B
Text
set_option backward.do.legacy false
|
|
def f1 (x : Nat) : IO Unit := do
|
|
IO.println x
|
|
return ()
|
|
|
|
def g1 : IO Unit := do
|
|
f1 -- Error
|
|
pure ()
|
|
|
|
def f2 (x : Nat) (y : Nat) : IO Unit := do
|
|
IO.println s!"{x} {y}"
|
|
return ()
|
|
|
|
def g2 : IO Unit := do
|
|
f2 10 -- Error
|
|
pure ()
|