mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
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
241 B
Lean4
8 lines
241 B
Lean4
set_option backward.do.legacy false
|
||
def g (xs ys : List Nat) (a : α) : IO Nat := do
|
||
let mut sum := 0
|
||
for x in xs, y in ys, c in a, z in ys do
|
||
sum := x + sum
|
||
IO.println s!"x: {x}, y: {y}, a: {a}, c: {c}, sum: {sum}"
|
||
return sum
|