chore: use hasNoConfusionDecl in grind

leanprover · Jan 21, 2025 · 6fcce8f · 6fcce8f
1 parent 57e7693
commit 6fcce8f
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/src/Lean/Meta/Tactic/Grind/Ctor.lean b/src/Lean/Meta/Tactic/Grind/Ctor.lean
@@ -46,8 +46,7 @@ def propagateCtor (a b : Expr) : GoalM Unit := do
     propagateInjEqs (← inferType injLemma) injLemma
   else
     let .const declName _ := aType.getAppFn | return ()
-    let noConfusionDeclName := Name.mkStr declName "noConfusion"
-    unless (← getEnv).contains noConfusionDeclName do return ()
+    unless (← hasNoConfusionDecl declName) do return ()
     closeGoal (← mkNoConfusion (← getFalseExpr) (← mkEqProof a b))
 
 end Lean.Meta.Grind