From 9290a0e9b13c7873d6aca02eba3d38f1043bb95d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 31 May 2022 18:17:56 -0700
Subject: [PATCH] chore: fix tests

---
 tests/lean/1074b.lean.expected.out             | 4 ++--
 tests/lean/255.lean.expected.out               | 4 ++--
 tests/lean/StxQuot.lean.expected.out           | 2 +-
 tests/lean/defInst.lean.expected.out           | 2 +-
 tests/lean/nameArgErrorIssue.lean.expected.out | 2 +-
 tests/lean/namedHoles.lean.expected.out        | 4 ++--
 6 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/tests/lean/1074b.lean.expected.out b/tests/lean/1074b.lean.expected.out
index 2b7e9055a6..16fe748212 100644
--- a/tests/lean/1074b.lean.expected.out
+++ b/tests/lean/1074b.lean.expected.out
@@ -1,9 +1,9 @@
 1074b.lean:10:30-10:31: error: unknown identifier 'z'
 1074b.lean:11:43-11:53: error: tactic 'assumption' failed
 a n : Term
-⊢ Brx (sorryAx Term)
+⊢ Brx (sorryAx Term true)
 1074b.lean:11:9-11:55: error: unsolved goals
 case id
 a n z✝ : Term
 : Brx z✝
-⊢ True ∧ Brx (sorryAx Term)
+⊢ True ∧ Brx (sorryAx Term true)
diff --git a/tests/lean/255.lean.expected.out b/tests/lean/255.lean.expected.out
index 1bb006b489..907805e394 100644
--- a/tests/lean/255.lean.expected.out
+++ b/tests/lean/255.lean.expected.out
@@ -1,6 +1,6 @@
 id x : α
 id x✝ : α
 255.lean:16:7-16:8: error: unknown constant 'x✝'
-id (sorryAx ?m) : ?m
+id (sorryAx ?m true) : ?m
 255.lean:20:9-20:10: error: unknown constant 'x✝'
-id (sorryAx ?m) : ?m
+id (sorryAx ?m true) : ?m
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index cc50beb9a7..7ff382d7b6 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -44,7 +44,7 @@ StxQuot.lean:18:15: error: expected term
 "#[(num \"1\"), [(num \"2\") (num \"3\")], (num \"4\")]"
 "#[(num \"2\")]"
 StxQuot.lean:94:39-94:44: error: unexpected antiquotation splice
-fun a => sorryAx (?m a) : (a : ?m) → ?m a
+fun a => sorryAx (?m a) true : (a : ?m) → ?m a
 "#[(some 1), (some 2)]"
 StxQuot.lean:101:13-101:14: error: unknown identifier 'x' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.
 "`id._@.UnhygienicMain._hyg.1"
diff --git a/tests/lean/defInst.lean.expected.out b/tests/lean/defInst.lean.expected.out
index 8a93131a95..126cd16e2c 100644
--- a/tests/lean/defInst.lean.expected.out
+++ b/tests/lean/defInst.lean.expected.out
@@ -1,7 +1,7 @@
 [4, 5, 6]
 defInst.lean:8:26-8:32: error: failed to synthesize instance
   BEq Foo
-fun x y => sorryAx (?m x y) : (x y : Foo) → ?m x y
+fun x y => sorryAx (?m x y) true : (x y : Foo) → ?m x y
 [4, 5, 6]
 fun x y => x == y : Foo → Foo → Bool
 [("hello", "hello")]
diff --git a/tests/lean/nameArgErrorIssue.lean.expected.out b/tests/lean/nameArgErrorIssue.lean.expected.out
index 13f3fa9776..80768a7573 100644
--- a/tests/lean/nameArgErrorIssue.lean.expected.out
+++ b/tests/lean/nameArgErrorIssue.lean.expected.out
@@ -7,7 +7,7 @@ has type
   String : Type
 but is expected to have type
   Nat : Type
-bla (sorryAx Nat) 5 : Nat
+bla (sorryAx Nat true) 5 : Nat
 nameArgErrorIssue.lean:6:20-6:24: error: application type mismatch
   bla "hi"
 argument
diff --git a/tests/lean/namedHoles.lean.expected.out b/tests/lean/namedHoles.lean.expected.out
index 911fff47d0..626a786aea 100644
--- a/tests/lean/namedHoles.lean.expected.out
+++ b/tests/lean/namedHoles.lean.expected.out
@@ -6,13 +6,13 @@ has type
   Nat : Type
 but is expected to have type
   Bool : Type
-f ?x (sorryAx Bool) : Nat
+f ?x (sorryAx Bool true) : Nat
 g ?x ?x : Nat
 20
 foo (fun x => ?m x) ?hole : Nat
 bla ?hole fun x => ?hole : Nat
 namedHoles.lean:35:38-35:43: error: synthetic hole has already been defined with an incompatible local context
-boo (fun x => ?m x) fun y => sorryAx Nat : Nat
+boo (fun x => ?m x) fun y => sorryAx Nat true : Nat
 11
 12
 namedHoles.lean:58:26-58:31: error: synthetic hole has already been defined and assigned to value incompatible with the current context