From 9d0a4d21d40f80dc8af32159810ba82d89e5c4ca Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 4 Sep 2014 10:00:42 -0700
Subject: [PATCH] chore(tests/lean/interactive): adjust test expected output

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

diff --git a/tests/lean/interactive/t4.input.expected.out b/tests/lean/interactive/t4.input.expected.out
index 3538a731b..dfd713373 100644
--- a/tests/lean/interactive/t4.input.expected.out
+++ b/tests/lean/interactive/t4.input.expected.out
@@ -5,6 +5,11 @@
 -- IDENTIFIER|6|6
 epsilon
 -- ACK
+-- EXTRA_TYPE|6|14
+λ (x : nat), true
+--
+nat → Prop
+-- ACK
 -- SYMBOL|6|14
 (
 -- ACK