From 42b5b1e67900f70373b222823224d4233f96b17a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 22 Jan 2015 11:41:19 -0800
Subject: [PATCH] test(tests/lean): add new test for scoping rules

---
 tests/lean/sec2.lean              | 24 ++++++++++++++++++++++++
 tests/lean/sec2.lean.expected.out | 13 +++++++++++++
 2 files changed, 37 insertions(+)
 create mode 100644 tests/lean/sec2.lean
 create mode 100644 tests/lean/sec2.lean.expected.out

diff --git a/tests/lean/sec2.lean b/tests/lean/sec2.lean
new file mode 100644
index 000000000..efae2f972
--- /dev/null
+++ b/tests/lean/sec2.lean
@@ -0,0 +1,24 @@
+structure A : Type := mk
+structure B : Type := mk
+constant f : A → B
+constant g : B → B
+constant a : A
+
+namespace foo
+  coercion f
+  print coercions
+  check g a
+end foo
+
+check g a -- Error
+
+section boo
+  coercion f
+  print coercions
+  check g a
+end boo
+-- The metaobjects defined in the section persist to the outer level.
+-- This is not a bug. The idea is: we can use the scope to define
+-- auxiliary variables that are then used to define classes/instances/etc.
+-- That is, the whole point of the scope is to define these metaobjects.
+check g a -- Ok
diff --git a/tests/lean/sec2.lean.expected.out b/tests/lean/sec2.lean.expected.out
new file mode 100644
index 000000000..f5e465157
--- /dev/null
+++ b/tests/lean/sec2.lean.expected.out
@@ -0,0 +1,13 @@
+A ↣ B : f
+g a : B
+sec2.lean:13:6: error: type mismatch at application
+  g a
+term
+  a
+has type
+  A
+but is expected to have type
+  B
+A ↣ B : f
+g a : B
+g a : B