From 7a0cbdbe0437e9aa769b1b1486891732ea96e560 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Oct 2020 11:51:17 -0700
Subject: [PATCH] test: shadowing in `do` blocks

---
 tests/lean/run/doNotation2.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/tests/lean/run/doNotation2.lean b/tests/lean/run/doNotation2.lean
index 0fed9216c7..9b168186e9 100644
--- a/tests/lean/run/doNotation2.lean
+++ b/tests/lean/run/doNotation2.lean
@@ -30,3 +30,17 @@ rfl
 
 theorem ex2 : (g [] $.run' 0) = 1 :=
 rfl
+
+def h (x : Nat) (y : Nat) : Nat := do
+if x > 0 then
+  let y := x + 1 -- this is a new `y` that shadows the one above
+  x := y
+else
+  y := y + 1
+return x + y
+
+theorem ex3 (y : Nat) : h 0 y = 0 + (y + 1) :=
+rfl
+
+theorem ex4 (y : Nat) : h 1 y = (1 + 1) + y :=
+rfl