aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

fix: Use guarded `isDefEq`

This commit is contained in:
Leni Aniva 2024-12-09 00:06:20 -08:00
parent 17ab2eafd8
commit 2d068ecd50
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Pantograph/Frontend/Elab.lean
View File

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