diff --git a/tests/lean/run/root.lean b/tests/lean/run/root.lean
new file mode 100644
index 0000000000..9eacc12c4b
--- /dev/null
+++ b/tests/lean/run/root.lean
@@ -0,0 +1,17 @@
+def x := 10
+
+
+namespace Foo
+
+def x := true
+
+#check x
+#check _root_.x
+
+theorem ex1 : x = true := rfl
+theorem ex2 : _root_.x = 10 := rfl
+
+end Foo
+
+theorem ex3 : x = 10 := rfl
+theorem ex4 : _root_.x = 10 := rfl