From 74a8b5f2f4c24bd359d738523915766bff474756 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Dec 2013 17:19:53 -0800
Subject: [PATCH] test(tests/lean/interactive): add back command test

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

diff --git a/tests/lean/interactive/t3.lean b/tests/lean/interactive/t3.lean
new file mode 100644
index 000000000..37ca5de17
--- /dev/null
+++ b/tests/lean/interactive/t3.lean
@@ -0,0 +1,9 @@
+Theorem T2 (a b : Bool) : b => a \/ b.
+apply imp_tactic.
+apply disj_tactic.
+back.
+back.
+apply assumption_tactic.
+done.
+
+Show Environment 1.
\ No newline at end of file
diff --git a/tests/lean/interactive/t3.lean.expected.out b/tests/lean/interactive/t3.lean.expected.out
new file mode 100644
index 000000000..eac4ac983
--- /dev/null
+++ b/tests/lean/interactive/t3.lean.expected.out
@@ -0,0 +1,19 @@
+Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
+#   Set: pp::colors
+  Set: pp::unicode
+Proof state:
+a : Bool, b : Bool ⊢ b ⇒ a ∨ b
+## Proof state:
+H : b, a : Bool, b : Bool ⊢ a ∨ b
+## Proof state:
+H : b, a : Bool, b : Bool ⊢ a
+## Proof state:
+H : b, a : Bool, b : Bool ⊢ b
+## Error (line: 8, pos: 0) failed to backtrack
+Proof state:
+H : b, a : Bool, b : Bool ⊢ b
+## Proof state:
+no goals
+##   Proved: T2
+# Theorem T2 (a b : Bool) : b ⇒ a ∨ b := Discharge (λ H : b, Disj2 a H)
+# 
\ No newline at end of file