From d8ced44ce23dc0dff9c1e1a4202cdd484e7be866 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 31 Jan 2021 09:01:08 -0800
Subject: [PATCH] test: fix test

Error is now caught by the elaborator too
---
 tests/lean/modBug.lean.expected.out | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/tests/lean/modBug.lean.expected.out b/tests/lean/modBug.lean.expected.out
index 94945a5293..389d68e4a0 100644
--- a/tests/lean/modBug.lean.expected.out
+++ b/tests/lean/modBug.lean.expected.out
@@ -1,6 +1,8 @@
-modBug.lean:1:8-1:20: error: application type mismatch
+modBug.lean:1:32-1:61: error: application type mismatch
   Nat.zeroNeOne (Nat.modZero 1)
-argument has type
+argument
+  Nat.modZero 1
+has type
   1 % 0 = 1
-but function has type
-  0 = 1 → False
+but is expected to have type
+  0 = 1