From e9d8a960d9f99010a25a14041cb539588fbd0909 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 29 Jan 2015 16:44:10 -0800
Subject: [PATCH] test(tests/lean/interactive): add test for proof_state info

---
 .../lean/interactive/proof_state_info3.input  | 19 ++++++++++++
 .../proof_state_info3.input.expected.out      | 30 +++++++++++++++++++
 2 files changed, 49 insertions(+)
 create mode 100644 tests/lean/interactive/proof_state_info3.input
 create mode 100644 tests/lean/interactive/proof_state_info3.input.expected.out

diff --git a/tests/lean/interactive/proof_state_info3.input b/tests/lean/interactive/proof_state_info3.input
new file mode 100644
index 000000000..b4af4f92d
--- /dev/null
+++ b/tests/lean/interactive/proof_state_info3.input
@@ -0,0 +1,19 @@
+VISIT proof_state_info3.lean
+SYNC 11
+
+
+theorem tst (a b c : Prop) : a → b → a ∧ b :=
+begin
+  info,
+  intros (Ha, Hb),
+  info,
+  apply and.intro,
+  apply Ha,
+  apply Hb,
+end
+WAIT
+REPLACE 7
+  state,
+SHOW
+WAIT
+INFO 8 17
\ No newline at end of file
diff --git a/tests/lean/interactive/proof_state_info3.input.expected.out b/tests/lean/interactive/proof_state_info3.input.expected.out
new file mode 100644
index 000000000..07524c2c6
--- /dev/null
+++ b/tests/lean/interactive/proof_state_info3.input.expected.out
@@ -0,0 +1,30 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINSHOW
+
+
+theorem tst (a b c : Prop) : a → b → a ∧ b :=
+begin
+  info,
+  intros (Ha, Hb),
+  state,
+  apply and.intro,
+  apply Ha,
+  apply Hb,
+end
+-- ENDSHOW
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGININFO
+-- PROOF_STATE|8|17
+a b c : Prop,
+Ha : a,
+Hb : b
+⊢ a
+--
+a b c : Prop,
+Ha : a,
+Hb : b
+⊢ b
+-- ACK
+-- ENDINFO