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

---
 .../lean/interactive/overload_coercion.input  | 11 ++++
 .../overload_coercion.input.expected.out      | 57 +++++++++++++++++++
 2 files changed, 68 insertions(+)
 create mode 100644 tests/lean/interactive/overload_coercion.input
 create mode 100644 tests/lean/interactive/overload_coercion.input.expected.out

diff --git a/tests/lean/interactive/overload_coercion.input b/tests/lean/interactive/overload_coercion.input
new file mode 100644
index 000000000..f7f6e967f
--- /dev/null
+++ b/tests/lean/interactive/overload_coercion.input
@@ -0,0 +1,11 @@
+VISIT overload_coercions.lean
+SYNC 6
+open nat num
+variable a : nat
+variable b : num
+variable c : bool
+check a + b
+check add a c
+WAIT
+INFO 5
+INFO 6
diff --git a/tests/lean/interactive/overload_coercion.input.expected.out b/tests/lean/interactive/overload_coercion.input.expected.out
new file mode 100644
index 000000000..464067eb0
--- /dev/null
+++ b/tests/lean/interactive/overload_coercion.input.expected.out
@@ -0,0 +1,57 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGININFO
+-- TYPE|5|6
+ℕ
+-- ACK
+-- IDENTIFIER|5|6
+a
+-- ACK
+-- TYPE|5|8
+ℕ → ℕ → ℕ
+-- ACK
+-- OVERLOAD|5|8
+num.add #1 #0
+--
+nat.add #1 #0
+-- ACK
+-- SYMBOL|5|8
++
+-- ACK
+-- IDENTIFIER|5|8
+nat.add
+-- ACK
+-- TYPE|5|10
+num
+-- ACK
+-- COERCION|5|10
+of_num b
+--
+ℕ
+-- ACK
+-- IDENTIFIER|5|10
+b
+-- ACK
+-- ENDINFO
+-- BEGININFO STALE
+-- TYPE|6|6
+ℕ → ℕ → ℕ
+-- ACK
+-- OVERLOAD|6|6
+num.add
+--
+nat.add
+-- ACK
+-- TYPE|6|10
+ℕ
+-- ACK
+-- IDENTIFIER|6|10
+a
+-- ACK
+-- TYPE|6|12
+bool
+-- ACK
+-- IDENTIFIER|6|12
+c
+-- ACK
+-- ENDINFO