is simpMatchWF needed?

leanprover · May 13, 2024 · cbdc0c5 · cbdc0c5
1 parent 787b221
commit cbdc0c5
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
@@ -9,6 +9,7 @@ import Lean.Meta.Tactic.Split
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Eqns
 import Lean.Meta.ArgsPacker.Basic
+import Init.Data.Array.Basic
 
 namespace Lean.Elab.WF
 open Meta
@@ -71,7 +72,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
         return ()
       else if (← tryContradiction mvarId) then
         return ()
-      else if let some mvarId ← simpMatchWF? mvarId then
+      else if let some mvarId ← simpMatch? mvarId then
         go mvarId
       else if let some mvarId ← simpIf? mvarId then
         go mvarId