diff --git a/tests/lean/using.lean b/tests/lean/using.lean
new file mode 100644
index 000000000..5cd9475a3
--- /dev/null
+++ b/tests/lean/using.lean
@@ -0,0 +1,17 @@
+scope
+   using Nat
+   print add 0 1
+   check add_assoc
+end
+
+print add 0 1
+
+namespace foo
+    using Nat
+    print add 0 1
+end
+
+using Nat::add plus
+check plus_assoc
+
+print add 0 1
diff --git a/tests/lean/using.lean.expected.out b/tests/lean/using.lean.expected.out
new file mode 100644
index 000000000..eb09767d4
--- /dev/null
+++ b/tests/lean/using.lean.expected.out
@@ -0,0 +1,11 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Using: Nat
+0 + 1
+Nat::add_assoc : ∀ a b c : ℕ, a + (b + c) = a + b + c
+using.lean:7:6: error: unknown identifier 'add'
+  Using: Nat
+0 + 1
+  Using: Nat::add as plus
+using.lean:15:6: error: unknown identifier 'plus_assoc'
+using.lean:17:6: error: unknown identifier 'add'