From 59d3227eaa82959993fc6d588fa128d5a3156970 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Aug 2014 18:16:41 -0700
Subject: [PATCH] fix(tests/lean/interactive): test output

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/interactive/in4.input.expected.out | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/tests/lean/interactive/in4.input.expected.out b/tests/lean/interactive/in4.input.expected.out
index f6146fdf9..679701599 100644
--- a/tests/lean/interactive/in4.input.expected.out
+++ b/tests/lean/interactive/in4.input.expected.out
@@ -14,5 +14,10 @@ rfl
 -- NAY
 -- ENDINFO
 -- BEGININFO
--- NAY
+-- TYPE|9|0
+∀ (a : A), eq a a
+-- ACK
+-- SYMBOL|9|0
+rfl
+-- ACK
 -- ENDINFO