From a6063a5560d01983a1584d69ca79ec19270635ae Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Oct 2020 11:28:52 -0700
Subject: [PATCH] chore: fix tests

---
 tests/lean/dbgMacros.lean.expected.out               | 2 +-
 tests/lean/phashmap_inst_coherence.lean.expected.out | 8 ++++----
 tests/lean/protected.lean.expected.out               | 8 ++++----
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/tests/lean/dbgMacros.lean.expected.out b/tests/lean/dbgMacros.lean.expected.out
index 9ff67e4b9b..6a523446e2 100644
--- a/tests/lean/dbgMacros.lean.expected.out
+++ b/tests/lean/dbgMacros.lean.expected.out
@@ -1,12 +1,12 @@
 PANIC at f dbgMacros:4:14: unexpected zero
 PANIC at g dbgMacros:12:14: unreachable code has been reached
 PANIC at h dbgMacros:18:0: assertion violation: x != 0
-f2, x: 10
 0
 9
 0
 0
 0
+f2, x: 10
 11
 g2 started
 11
diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out
index 81a0cf9926..bd31bf8fae 100644
--- a/tests/lean/phashmap_inst_coherence.lean.expected.out
+++ b/tests/lean/phashmap_inst_coherence.lean.expected.out
@@ -9,10 +9,10 @@ but is expected to have type
 failed to synthesize instance
   CoeT (PersistentHashMap Nat Nat) m (PersistentHashMap Nat Nat)
 phashmap_inst_coherence.lean:12:0: error: application type mismatch
-  Lean.runEval (sorryAx ?m)
+  Lean.runEval fun («_» : Unit) => sorryAx ?m
 argument
-  sorryAx ?m
+  fun («_» : Unit) => sorryAx ?m
 has type
-  ?m
+  Unit → ?m
 but is expected to have type
-  ?m
+  Unit → ?m
diff --git a/tests/lean/protected.lean.expected.out b/tests/lean/protected.lean.expected.out
index 3c822dffbb..63d8067cce 100644
--- a/tests/lean/protected.lean.expected.out
+++ b/tests/lean/protected.lean.expected.out
@@ -11,11 +11,11 @@ protected.lean:28:14: error: unknown identifier 'f'
 protected.lean:38:14: error: unknown identifier 'g'
 protected.lean:47:6: error: unknown identifier 'g'
 protected.lean:47:0: error: application type mismatch
-  Lean.runEval (sorryAx ?m)
+  Lean.runEval fun («_» : Unit) => sorryAx ?m
 argument
-  sorryAx ?m
+  fun («_» : Unit) => sorryAx ?m
 has type
-  ?m
+  Unit → ?m
 but is expected to have type
-  ?m
+  Unit → ?m
 8