From 9c9cad6ae8020dd16e15097716072f146811a965 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Jan 2017 21:48:19 -0800
Subject: [PATCH] test(tests/lean/interactive): add regression test for #1313

---
 tests/lean/interactive/1313.lean              | 34 +++++++++++++++++++
 tests/lean/interactive/1313.lean.expected.out | 11 ++++++
 2 files changed, 45 insertions(+)
 create mode 100644 tests/lean/interactive/1313.lean
 create mode 100644 tests/lean/interactive/1313.lean.expected.out

diff --git a/tests/lean/interactive/1313.lean b/tests/lean/interactive/1313.lean
new file mode 100644
index 0000000000..6f729d946a
--- /dev/null
+++ b/tests/lean/interactive/1313.lean
@@ -0,0 +1,34 @@
+example (p q : Prop) (a : p) (b : q) : p ∧ q ∧ p :=
+begin
+
+--^ "command": "info"
+end
+
+
+example (p q : Prop) (a : p) (b : q) : p ∧ q ∧ p :=
+begin
+apply and.intro,
+             --^ "command": "info"
+end
+
+example (p q : Prop) (a : p) (b : q) : p ∧ q ∧ p :=
+begin
+apply and.intro,
+               --^ "command": "info"
+end
+
+example (p q : Prop) (a : p) (b : q) : p ∧ q ∧ p :=
+begin
+apply and.intro,
+
+--^ "command": "info"
+end
+
+
+example (p q : Prop) (a : p) (b : q) : p ∧ q ∧ p :=
+begin
+apply and.intro,
+
+--^ "command": "info"
+{exact a},
+end
diff --git a/tests/lean/interactive/1313.lean.expected.out b/tests/lean/interactive/1313.lean.expected.out
new file mode 100644
index 0000000000..707a0393d1
--- /dev/null
+++ b/tests/lean/interactive/1313.lean.expected.out
@@ -0,0 +1,11 @@
+{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":5,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},"response":"additional_message"}
+{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":12,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
+{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":18,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
+{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":25,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
+{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":34,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
+{"message":"file invalidated","response":"ok","seq_num":0}
+{"record":{"state":"p q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},"response":"ok","seq_num":4}
+{"record":{"state":"p q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"ok","seq_num":11}
+{"record":{"state":"p q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"ok","seq_num":17}
+{"record":{"state":"p q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"ok","seq_num":24}
+{"record":{"state":"p q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"ok","seq_num":32}