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>
10 lines
273 B
Text
10 lines
273 B
Text
set_option backward.do.legacy false
|
|
def foo1 : IO Unit := do
|
|
let f (x : IO.Ref Nat) : IO Nat :=
|
|
pure ((← x.get) + 1)
|
|
IO.println (IO.mkRef 10)
|
|
|
|
def foo2 : IO Unit := do
|
|
let rec f (x : IO.Ref Nat) : IO Nat :=
|
|
pure ((← x.get) + 1)
|
|
IO.println (IO.mkRef 10)
|