chore: fix tests

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)

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

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"

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")]

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

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