From 765a8ac984f100cd7eb3ade06b1e0ba5cd58a001 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Sep 2020 12:41:33 -0700 Subject: [PATCH] test: `do` with optional `;` --- tests/lean/run/doNotation2.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 tests/lean/run/doNotation2.lean diff --git a/tests/lean/run/doNotation2.lean b/tests/lean/run/doNotation2.lean new file mode 100644 index 0000000000..2fa9d98fb6 --- /dev/null +++ b/tests/lean/run/doNotation2.lean @@ -0,0 +1,17 @@ +new_frontend + +def f (x : Nat) : IO Nat := do +IO.println "hello world" +let aux (y : Nat) (z : Nat) : IO Nat := do + IO.println "aux started" + IO.println ("y: " ++ toString y ++ ", z: " ++ toString z) + return x+y +aux x + (x + 1) -- It is part of the application since it is indented +aux x (x -- parentheses use `withoutPosition` +-1) +aux x x; + aux x + x + +#eval f 10