From 5d515a06f74bc56782574c837c9046416271c909 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 5 May 2015 18:32:21 -0700
Subject: [PATCH] test(tests/lean/run): add test showing that "proof ... qed"
 can access the whole context

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

diff --git a/tests/lean/run/proof_qed_improved.lean b/tests/lean/run/proof_qed_improved.lean
new file mode 100644
index 000000000..79dd6ea81
--- /dev/null
+++ b/tests/lean/run/proof_qed_improved.lean
@@ -0,0 +1,6 @@
+example (a b c : nat) (f : nat → nat → nat) (H₁ : a = b) (H₂ : b = c) : f (f a a) (f b b) = f (f c c) (f c c) :=
+have h : a = c, from eq.trans H₁ H₂,
+proof
+  calc f (f a a) (f b b) = f (f c c) (f b b) : by rewrite h
+                   ...   = f (f c c) (f c c) : by rewrite H₂
+qed