From 2d068ecd5072386fd4043931b96e64fd47760aab Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 00:06:20 -0800
Subject: [PATCH] fix: Use guarded `isDefEq`

---
 Pantograph/Frontend/Elab.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index d5af8b5..c4704fc 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -110,7 +110,7 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext)
         return true
       ctx.runMetaM lctx do
         let type ← Meta.inferType expr
-        Bool.not <$> Meta.isDefEq type expectedType
+        Bool.not <$> Meta.isExprDefEqGuarded type expectedType
     | .ofTacticInfo { stx, goalsBefore, .. } =>
       -- The `sorry` term is distinct from the `sorry` tactic
       let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry