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>
33 lines
668 B
Text
33 lines
668 B
Text
set_option backward.do.legacy false
|
|
def f : IO Nat := do
|
|
IO.println "hello"
|
|
IO.getStdin
|
|
return 10
|
|
|
|
def f1 : ExceptT String (StateT Nat Id) Nat := do
|
|
modify (· + 1)
|
|
get
|
|
|
|
def f2 (x : Nat) : ExceptT String (StateT Nat Id) Nat := do
|
|
modify (· + x)
|
|
get
|
|
|
|
def g1 : ExceptT String (StateT Nat Id) Unit := do
|
|
let x : String ← f1
|
|
return ()
|
|
|
|
def g2 : ExceptT String (StateT Nat Id) Unit := do
|
|
let x : String ← f2 10
|
|
return ()
|
|
|
|
def g3 : ExceptT String (StateT Nat Id) String := do
|
|
let x ← f2
|
|
f1
|
|
|
|
example : Nat := Id.run do
|
|
let mut n : Nat := 0
|
|
n := false
|
|
n : Char := false
|
|
(n, _) := (false, false)
|
|
((n : Char), _) := (false, false)
|
|
n
|