mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
14 lines
278 B
Lean4
14 lines
278 B
Lean4
def initX : IO (IO.Ref Nat) :=
|
|
IO.mkRef 0
|
|
|
|
@[init initX] constant x : IO.Ref Nat := default _
|
|
|
|
def inc : IO Unit :=
|
|
do v ← x.get,
|
|
x.set (v+1),
|
|
IO.println (">> " ++ toString v)
|
|
|
|
def main (xs : List String) : IO Unit :=
|
|
do let n := xs.head.toNat,
|
|
n.mrepeat (λ _, inc)
|