From 52e11dbbee60ec5f4001f68b7040ec0e25615743 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 9 Jan 2014 12:21:14 -0800
Subject: [PATCH] test(tests/lean): 'using' command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/using.lean              | 17 +++++++++++++++++
 tests/lean/using.lean.expected.out | 11 +++++++++++
 2 files changed, 28 insertions(+)
 create mode 100644 tests/lean/using.lean
 create mode 100644 tests/lean/using.lean.expected.out

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'