From 1b4d2a850afd4e95d75db18e39dd759ae4cf4cde Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Mon, 30 Oct 2017 14:31:37 -0400
Subject: [PATCH] test(focus): add test

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

diff --git a/tests/lean/run/focus.lean b/tests/lean/run/focus.lean
new file mode 100644
index 0000000000..2032cfa07d
--- /dev/null
+++ b/tests/lean/run/focus.lean
@@ -0,0 +1,12 @@
+open nat
+example (n m : ℕ) : n + m = m + n :=
+begin
+  induction m with m IHm,
+  focus { induction n with n IHn,
+    focus { reflexivity },
+    focus { exact congr_arg succ IHn }},
+  focus { apply eq.trans (congr_arg succ IHm),
+    clear IHm, induction n with n IHn,
+    focus { reflexivity },
+    focus { exact congr_arg succ IHn }}
+end
\ No newline at end of file