From 851444b77a35981c006682f86e03af8b93c17e79 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 15 Sep 2014 16:07:23 -0700
Subject: [PATCH] test(tests/lean/interactive): test for issue #193

---
 tests/lean/interactive/alias.input            | 15 ++++++++++
 .../lean/interactive/alias.input.expected.out | 28 +++++++++++++++++++
 2 files changed, 43 insertions(+)
 create mode 100644 tests/lean/interactive/alias.input
 create mode 100644 tests/lean/interactive/alias.input.expected.out

diff --git a/tests/lean/interactive/alias.input b/tests/lean/interactive/alias.input
new file mode 100644
index 000000000..04f039f4e
--- /dev/null
+++ b/tests/lean/interactive/alias.input
@@ -0,0 +1,15 @@
+VISIT alias.lean
+SET
+pp.notation false
+REPLACE 1
+import data.bool
+WAIT
+FINDP 1
+tt
+REPLACE 2
+open bool
+REPLACE 3
+check tt
+WAIT
+FINDP 3
+tt
diff --git a/tests/lean/interactive/alias.input.expected.out b/tests/lean/interactive/alias.input.expected.out
new file mode 100644
index 000000000..7c6b70f4a
--- /dev/null
+++ b/tests/lean/interactive/alias.input.expected.out
@@ -0,0 +1,28 @@
+-- BEGINSET
+-- ENDSET
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINFINDP
+bool.bor_tt_left|∀ (a : bool), eq (bool.bor bool.tt a) bool.tt
+bool.tt|bool
+bool.bor_tt_right|∀ (a : bool), eq (bool.bor a bool.tt) bool.tt
+bool.band_tt_left|∀ (a : bool), eq (bool.band bool.tt a) a
+bool.band_tt_right|∀ (a : bool), eq (bool.band a bool.tt) a
+bool.cond_tt|∀ (t e : ?A), eq (bool.cond bool.tt t e) t
+bool.ff_ne_tt|not (eq bool.ff bool.tt)
+bool.band_eq_tt_elim_left|eq (bool.band ?a ?b) bool.tt → eq ?a bool.tt
+bool.band_eq_tt_elim_right|eq (bool.band ?a ?b) bool.tt → eq ?b bool.tt
+-- ENDFINDP
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINFINDP
+tt|bool
+bor_tt_left|∀ (a : bool), eq (bor tt a) tt
+bor_tt_right|∀ (a : bool), eq (bor a tt) tt
+band_tt_left|∀ (a : bool), eq (band tt a) a
+band_tt_right|∀ (a : bool), eq (band a tt) a
+cond_tt|∀ (t e : ?A), eq (cond tt t e) t
+ff_ne_tt|not (eq ff tt)
+band_eq_tt_elim_left|eq (band ?a ?b) tt → eq ?a tt
+band_eq_tt_elim_right|eq (band ?a ?b) tt → eq ?b tt
+-- ENDFINDP