From 6b81123dd0dca131be8df727f9110fe08cfa4308 Mon Sep 17 00:00:00 2001
From: Marc Huisinga <mhuisi@protonmail.com>
Date: Fri, 24 Jan 2025 18:46:33 +0100
Subject: [PATCH] test: adjust infotree output

---
 tests/lean/1018unknowMVarIssue.lean.expected.out | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out
index b6e967b1d559..b86ae35fcdc7 100644
--- a/tests/lean/1018unknowMVarIssue.lean.expected.out
+++ b/tests/lean/1018unknowMVarIssue.lean.expected.out
@@ -26,7 +26,8 @@ a : α
       • β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
         • [.] β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩
         • β : Type @ ⟨7, 33⟩-⟨7, 34⟩
-      • _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†-⟨10, 19⟩†
+      • InlayHint @ 170 =>  {α β}
+      • _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†!-⟨7, 7⟩†!
       • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
       • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
       • CustomInfo(Lean.Elab.Term.BodyInfo)