From 7073f036d8ff6270039a77f4b1614d9a0ac6f528 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 4 Oct 2014 08:15:43 -0700
Subject: [PATCH] test(tests/lean/run): add additional tests for section
 parameter/variable and strict implicit argument

---
 tests/lean/run/sec_var.lean | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 tests/lean/run/sec_var.lean

diff --git a/tests/lean/run/sec_var.lean b/tests/lean/run/sec_var.lean
new file mode 100644
index 000000000..a004a59ff
--- /dev/null
+++ b/tests/lean/run/sec_var.lean
@@ -0,0 +1,27 @@
+import logic
+
+section
+  parameter A : Type
+  definition foo : ∀ ⦃ a b : A ⦄, a = b → a = b :=
+  take a b H, H
+
+  variable a : A
+  set_option pp.implicit true
+  check foo (eq.refl a)
+  check foo
+  check foo = (λ (a b : A) (H : a = b), H)
+end
+
+check foo = (λ (A : Type) (a b : A) (H : a = b), H)
+
+section
+  variable A : Type
+  definition foo2 : ∀ ⦃ a b : A ⦄, a = b → a = b :=
+  take a b H, H
+
+  variable a : A
+  set_option pp.implicit true
+  check foo2 A (eq.refl a)
+  check foo2
+  check foo2 A = (λ (a b : A) (H : a = b), H)
+end