From 970ebd2b9180b9ef1d4e361a85b654943f4d6ea2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Mar 2019 15:52:36 -0700 Subject: [PATCH] test(tests/playground/ref2): small example using `[init]` --- tests/playground/ref2.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 tests/playground/ref2.lean diff --git a/tests/playground/ref2.lean b/tests/playground/ref2.lean new file mode 100644 index 0000000000..0a4f3e11df --- /dev/null +++ b/tests/playground/ref2.lean @@ -0,0 +1,13 @@ +def init_x : io (io.ref nat) := +io.mk_ref 0 + +@[init init_x] constant x : io.ref nat := default _ + +def inc : io unit := +do v ← x.read, + x.write (v+1), + io.println (">> " ++ to_string v) + +def main (xs : list string) : io unit := +do let n := xs.head.to_nat, + n.mrepeat (λ _, inc)