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>
24 lines
507 B
Text
24 lines
507 B
Text
set_option backward.do.legacy false
|
|
def f (x : Nat) : IO Unit := do
|
|
x -- Error
|
|
IO.println x
|
|
|
|
def f' (x : Nat) : IO Unit := do
|
|
discard (pure x)
|
|
IO.println x
|
|
|
|
def g (xs : Array Nat) : IO Unit := do
|
|
xs.set! 0 1 -- Error
|
|
IO.println xs
|
|
|
|
def g' (xs : Array Nat) : IO Unit := do
|
|
discard <| pure (xs.set! 0 1)
|
|
IO.println xs
|
|
|
|
def h (xs : Array Nat) : IO Unit := do
|
|
pure (xs.set! 0 1) -- Error
|
|
IO.println xs
|
|
|
|
def h' (xs : Array Nat) : IO Unit := do
|
|
discard <| pure (xs.set! 0 1)
|
|
IO.println xs
|