diff --git a/tests/compiler/expr.lean.expected.out b/tests/compiler/expr.lean.expected.out
index 48aa4662c7..5c2981c9a9 100644
--- a/tests/compiler/expr.lean.expected.out
+++ b/tests/compiler/expr.lean.expected.out
@@ -1,3 +1,3 @@
 f a b
-hash: 4194966675
+hash: 3375555335
 #[a, b]
diff --git a/tests/lean/450.lean.expected.out b/tests/lean/450.lean.expected.out
index 2ba2013d9e..8017fe9571 100644
--- a/tests/lean/450.lean.expected.out
+++ b/tests/lean/450.lean.expected.out
@@ -1,4 +1,4 @@
-450.lean:2:6-2:7: error: failed to infer 'let' declaration type
 450.lean:2:11-2:12: error: don't know how to synthesize placeholder
 context:
 ⊢ ?m
+450.lean:2:6-2:7: error: failed to infer 'let' declaration type
diff --git a/tests/lean/906.lean.expected.out b/tests/lean/906.lean.expected.out
index 14eba0009c..e26403110e 100644
--- a/tests/lean/906.lean.expected.out
+++ b/tests/lean/906.lean.expected.out
@@ -1,3 +1,2 @@
 906.lean:2:4-2:15: warning: declaration uses 'sorry'
-906.lean:12:2-12:28: error: tactic 'simp' failed, nested error:
-(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
+906.lean:12:2-12:28: error: maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)
diff --git a/tests/lean/CompilerElimDeadBranches.lean.expected.out b/tests/lean/CompilerElimDeadBranches.lean.expected.out
index 57bf7b9fe8..35d929a0bc 100644
--- a/tests/lean/CompilerElimDeadBranches.lean.expected.out
+++ b/tests/lean/CompilerElimDeadBranches.lean.expected.out
@@ -1,9 +1,9 @@
-[Compiler.elimDeadBranches] Eliminating addSomeVal._redArg with #[("_x.37",
+[Compiler.elimDeadBranches] Eliminating addSomeVal._redArg with #[("val.20", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
+      ("val.16", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
+      ("_x.37",
        Lean.Compiler.LCNF.UnreachableBranches.Value.ctor
          `Option.some
          #[Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]]),
-      ("val.20", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
-      ("val.16", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
       ("_x.35", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
       ("_x.36",
        Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top])]
@@ -47,22 +47,21 @@
           let _x.5 := some _ _x.4;
           return _x.5
 [Compiler.result] size: 1 def addSomeVal x : Option Nat := let _x.1 := addSomeVal._redArg; return _x.1
-[Compiler.elimDeadBranches] Eliminating monadic with #[("_x.207",
-       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
+[Compiler.elimDeadBranches] Eliminating monadic with #[("y", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("a.206", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
+      ("_x.91",
+       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.ok #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
       ("_x.88", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("a.208", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("val.200", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("_x.205",
-       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
-      ("val.64", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("_x.211",
-       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
-      ("y", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("a.206", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
       ("_x.212",
        Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
-      ("_x.91",
-       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.ok #[Lean.Compiler.LCNF.UnreachableBranches.Value.top])]
+      ("a.208", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
+      ("_x.211",
+       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
+      ("val.200", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
+      ("_x.207",
+       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
+      ("_x.205",
+       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
+      ("val.64", Lean.Compiler.LCNF.UnreachableBranches.Value.top)]
 [Compiler.elimDeadBranches] Threw away cases _x.211 branch Option.none
 [Compiler.elimDeadBranches] Threw away cases _x.212 branch Option.none
 [Compiler.elimDeadBranches] Threw away cases _x.205 branch Except.ok
diff --git a/tests/lean/argNameAtPlaceholderError.lean.expected.out b/tests/lean/argNameAtPlaceholderError.lean.expected.out
index d955d184eb..b30d8c8880 100644
--- a/tests/lean/argNameAtPlaceholderError.lean.expected.out
+++ b/tests/lean/argNameAtPlaceholderError.lean.expected.out
@@ -1,11 +1,11 @@
-argNameAtPlaceholderError.lean:8:13-8:14: error: don't know how to synthesize placeholder for argument 'expectedType?'
-context:
-stx : Syntax
-⊢ Option Expr
 argNameAtPlaceholderError.lean:8:15-8:16: error: don't know how to synthesize placeholder for argument 'catchExPostpone'
 context:
 stx : Syntax
 ⊢ Bool
+argNameAtPlaceholderError.lean:8:13-8:14: error: don't know how to synthesize placeholder for argument 'expectedType?'
+context:
+stx : Syntax
+⊢ Option Expr
 argNameAtPlaceholderError.lean:8:11-8:12: error: don't know how to synthesize placeholder for argument 'stx'
 context:
 stx : Syntax
diff --git a/tests/lean/derivingHashable.lean.expected.out b/tests/lean/derivingHashable.lean.expected.out
index e484a1a66b..b297051b01 100644
--- a/tests/lean/derivingHashable.lean.expected.out
+++ b/tests/lean/derivingHashable.lean.expected.out
@@ -1,4 +1,4 @@
-1182690223427565068
-4993501213146294156
-21469593610
-6073217436820174634
+10047522373567521337
+18299533346889728271
+5501096720095961210
+6693367456468911342
diff --git a/tests/lean/evalNone.lean.expected.out b/tests/lean/evalNone.lean.expected.out
index 7fdcd9ce11..f5abf4e7dc 100644
--- a/tests/lean/evalNone.lean.expected.out
+++ b/tests/lean/evalNone.lean.expected.out
@@ -2,11 +2,11 @@ evalNone.lean:1:6-1:10: error: don't know how to synthesize implicit argument
   @none ?m
 context:
 ⊢ Type ?u
-evalNone.lean:3:6-3:14: error: don't know how to synthesize implicit argument
-  @List.head? ?m []
-context:
-⊢ Type ?u
 evalNone.lean:3:6-3:8: error: don't know how to synthesize implicit argument
   @List.nil ?m
 context:
 ⊢ Type ?u
+evalNone.lean:3:6-3:14: error: don't know how to synthesize implicit argument
+  @List.head? ?m []
+context:
+⊢ Type ?u
diff --git a/tests/lean/hidingInaccessibleNames.lean.expected.out b/tests/lean/hidingInaccessibleNames.lean.expected.out
index 7df176e76c..de9da6ceed 100644
--- a/tests/lean/hidingInaccessibleNames.lean.expected.out
+++ b/tests/lean/hidingInaccessibleNames.lean.expected.out
@@ -14,11 +14,6 @@ context:
 x✝¹ : Nat
 x✝ : [] ≠ []
 ⊢ Nat
-hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder
-context:
-a b x✝¹ : Nat
-x✝ : [a, b] ≠ []
-⊢ Nat
 hidingInaccessibleNames.lean:8:16-8:17: error: don't know how to synthesize placeholder
 context:
 x✝¹ : Nat
@@ -30,6 +25,11 @@ x✝² : List Nat
 x✝¹ : Nat
 x✝ : x✝² ≠ []
 ⊢ Nat
+hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder
+context:
+a b x✝¹ : Nat
+x✝ : [a, b] ≠ []
+⊢ Nat
 case inl
 p q : Prop
 h✝ : p
diff --git a/tests/lean/holeErrors.lean.expected.out b/tests/lean/holeErrors.lean.expected.out
index b2c86aab89..caf9cdd707 100644
--- a/tests/lean/holeErrors.lean.expected.out
+++ b/tests/lean/holeErrors.lean.expected.out
@@ -1,22 +1,22 @@
-holeErrors.lean:3:11-3:20: error: failed to infer definition type
 holeErrors.lean:3:14-3:20: error: don't know how to synthesize implicit argument
   @id ?m
 context:
 ⊢ Sort u
+holeErrors.lean:3:11-3:20: error: failed to infer definition type
 holeErrors.lean:5:9-5:10: error: failed to infer definition type
 when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed
-holeErrors.lean:8:4-8:5: error: failed to infer 'let' declaration type
+holeErrors.lean:7:11-9:1: error: failed to infer definition type
 holeErrors.lean:8:9-8:15: error: don't know how to synthesize implicit argument
   @id ?m
 context:
 ⊢ Sort u
-holeErrors.lean:7:11-9:1: error: failed to infer definition type
-holeErrors.lean:11:11-11:15: error: failed to infer definition type
+holeErrors.lean:8:4-8:5: error: failed to infer 'let' declaration type
 holeErrors.lean:11:8-11:9: error: failed to infer binder type
+holeErrors.lean:11:11-11:15: error: failed to infer definition type
 holeErrors.lean:13:12-13:13: error: failed to infer binder type
 holeErrors.lean:13:15-13:19: error: failed to infer definition type
-holeErrors.lean:16:4-16:5: error: failed to infer binder type
 holeErrors.lean:15:7-16:10: error: failed to infer definition type
+holeErrors.lean:16:4-16:5: error: failed to infer binder type
 holeErrors.lean:19:13-19:19: error: don't know how to synthesize implicit argument
   @id ?m
 context:
diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out
index 1fbb76e993..5d7fd60fff 100644
--- a/tests/lean/holes.lean.expected.out
+++ b/tests/lean/holes.lean.expected.out
@@ -4,17 +4,17 @@ holes.lean:10:15-10:18: error: don't know how to synthesize implicit argument
 context:
 x : Nat
 ⊢ Type
-holes.lean:10:9-10:12: error: don't know how to synthesize implicit argument
-  @g Nat (?m x) x
-context:
-x : Nat
-⊢ Type
 holes.lean:11:8-11:13: error: don't know how to synthesize placeholder
 context:
 case hole
 x : Nat
 y : Nat := g x + g x
 ⊢ Nat
+holes.lean:10:9-10:12: error: don't know how to synthesize implicit argument
+  @g Nat (?m x) x
+context:
+x : Nat
+⊢ Type
 holes.lean:11:4-11:5: error: don't know how to synthesize placeholder
 context:
 x : Nat
@@ -22,12 +22,12 @@ y : Nat := g x + g x
 ⊢ Nat
 holes.lean:13:10-13:11: error: failed to infer binder type
 holes.lean:15:16-15:17: error: failed to infer binder type
+holes.lean:18:9-18:10: error: failed to infer binder type
 holes.lean:19:0-19:3: error: don't know how to synthesize implicit argument
   @f Nat (?m a) a
 context:
 a : Nat
 f : {α : Type} → {β : ?m a} → α → α := fun {α} {β} a => a
 ⊢ ?m a
-holes.lean:18:9-18:10: error: failed to infer binder type
 holes.lean:21:25-22:4: error: failed to infer definition type
 holes.lean:25:8-25:11: error: failed to infer 'let rec' declaration type
diff --git a/tests/lean/implicitTypePos.lean.expected.out b/tests/lean/implicitTypePos.lean.expected.out
index 7491818549..67464413a8 100644
--- a/tests/lean/implicitTypePos.lean.expected.out
+++ b/tests/lean/implicitTypePos.lean.expected.out
@@ -1,5 +1,5 @@
-implicitTypePos.lean:1:6-1:7: error: failed to infer binder type
 implicitTypePos.lean:1:8-1:9: error: failed to infer binder type
+implicitTypePos.lean:1:6-1:7: error: failed to infer binder type
 implicitTypePos.lean:3:9-3:10: error: failed to infer binder type
 implicitTypePos.lean:5:9-5:10: error: failed to infer binder type
 implicitTypePos.lean:7:10-7:11: error: failed to infer binder type
diff --git a/tests/lean/jason1.lean.expected.out b/tests/lean/jason1.lean.expected.out
index c75eebeb58..e94b6f7c10 100644
--- a/tests/lean/jason1.lean.expected.out
+++ b/tests/lean/jason1.lean.expected.out
@@ -1,53 +1,3 @@
-jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
-jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
-  @EGrfl
-    (getCtx
-      (TAlgebra
-        (@TySyntaxLayer.nat G T EG getCtx
-          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
-jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
-  @EGrfl
-    (getCtx
-      (TAlgebra
-        (@TySyntaxLayer.nat G T EG getCtx
-          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
 jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
   @TySyntaxLayer.arrow G T EG getCtx
     (getCtx
@@ -80,22 +30,12 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
-jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
-jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
+jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
+  @EGrfl
+    (getCtx
+      (TAlgebra
+        (@TySyntaxLayer.nat G T EG getCtx
+          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
 context:
 G T Tm : Type
 EG : G → G → Type
@@ -122,3 +62,63 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
+jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+Γ✝ : G
+⊢ G
+jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+Γ✝ : G
+⊢ G
+jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+Γ✝ : G
+⊢ G
+jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
+  @EGrfl
+    (getCtx
+      (TAlgebra
+        (@TySyntaxLayer.nat G T EG getCtx
+          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+Γ✝ : G
+⊢ G
diff --git a/tests/lean/jason2.lean.expected.out b/tests/lean/jason2.lean.expected.out
index 20d01eabe5..4ecd1be01f 100644
--- a/tests/lean/jason2.lean.expected.out
+++ b/tests/lean/jason2.lean.expected.out
@@ -1,8 +1,8 @@
-jason2.lean:4:30-4:37: error: don't know how to synthesize implicit argument
-  @Foo.foo ?m
-context:
-⊢ Nat
 jason2.lean:4:20-4:23: error: don't know how to synthesize implicit argument
   @Foo ?m
 context:
 ⊢ Nat
+jason2.lean:4:30-4:37: error: don't know how to synthesize implicit argument
+  @Foo.foo ?m
+context:
+⊢ Nat
diff --git a/tests/lean/multiConstantError.lean.expected.out b/tests/lean/multiConstantError.lean.expected.out
index ec62b813ad..4fe617b40f 100644
--- a/tests/lean/multiConstantError.lean.expected.out
+++ b/tests/lean/multiConstantError.lean.expected.out
@@ -1,6 +1,6 @@
-multiConstantError.lean:1:9-1:10: error: failed to infer binder type
-recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
 multiConstantError.lean:1:11-1:12: error: failed to infer binder type
 recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
+multiConstantError.lean:1:9-1:10: error: failed to infer binder type
+recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
 multiConstantError.lean:3:9-3:10: error: failed to infer binder type
 recall that you cannot declare multiple constants in a single declaration. The identifier(s) `α`, `β` are being interpreted as parameters `(α : _)`, `(β : _)`
diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean
index 6c58bc9246..1251ba682d 100644
--- a/tests/lean/run/match1.lean
+++ b/tests/lean/run/match1.lean
@@ -48,7 +48,6 @@ theorem ex3 {p q r : Prop} : p ∨ q → r → (q ∧ r) ∨ (p ∧ r) :=
 by intro
  | Or.inl hp, h => { apply Or.inr; apply And.intro; assumption; assumption }
  | Or.inr hq, h => { apply Or.inl; exact ⟨hq, h⟩ }
-#eval checkWithMkMatcherInput ``ex3.match_1
 
 inductive C
 | mk₁ : Nat → C
@@ -91,7 +90,7 @@ inductive Vec.{u} (α : Type u) : Nat → Type u
 def Vec.mapHead1 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ
 | _,   nil,       nil,       f => none
 | _, cons a as, cons b bs,   f => some (f a b)
-#eval checkWithMkMatcherInput ``Vec.mapHead1.match_1
+
 
 def Vec.mapHead2 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ
 | _, nil,            nil,         f => none
diff --git a/tests/pkg/user_ext/test.sh b/tests/pkg/user_ext/test.sh
index e130c3156d..6702875d7c 100755
--- a/tests/pkg/user_ext/test.sh
+++ b/tests/pkg/user_ext/test.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 
 rm -rf build
-lake build -v 2>&1 | grep 'world, hello, test'
+lake build -v 2>&1 | grep 'hello, world, test'