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>
8 lines
149 B
Text
8 lines
149 B
Text
set_option backward.do.legacy false
|
|
def f (x : Nat) : IO Nat := do
|
|
if x == 0 then
|
|
return 0
|
|
else if x then
|
|
return 1
|
|
else
|
|
return "a"
|