From 0a849003b23f3fa69099da8b59b8eaec01fc13f8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= <wojciech@lean-fro.org>
Date: Wed, 18 Feb 2026 22:49:25 +0000
Subject: [PATCH] refactor: remove dead matcher code from Cbv/Main.lean
 (#12568)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR removes `tryMatchEquations` and `tryMatcher` from
`Lean.Meta.Tactic.Cbv.Main`, as both are already defined and used in
`Lean.Meta.Tactic.Cbv.ControlFlow`. The copies in `Main.lean` were
unreachable dead code.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/Lean/Meta/Tactic/Cbv/Main.lean | 16 ----------------
 1 file changed, 16 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean
index ad1117e04c..fedec47fde 100644
--- a/src/Lean/Meta/Tactic/Cbv/Main.lean
+++ b/src/Lean/Meta/Tactic/Cbv/Main.lean
@@ -24,10 +24,6 @@ public register_builtin_option cbv.warning : Bool := {
   descr    := "disable `cbv` usage warning"
 }
 
-def tryMatchEquations (appFn : Name) : Simproc := fun e => do
-  let thms ← getMatchTheorems appFn
-  thms.rewrite (d := dischargeNone) e
-
 def tryEquations : Simproc := fun e => do
   unless e.isApp do
     return .rfl
@@ -42,18 +38,6 @@ def tryUnfold : Simproc := fun e => do
   let some thm ← getUnfoldTheorem appFn | return .rfl
   Theorem.rewrite thm e
 
-def tryMatcher : Simproc := fun e => do
-  unless e.isApp do
-    return .rfl
-  let some appFn := e.getAppFn.constName? | return .rfl
-  let some info ← getMatcherInfo? appFn | return .rfl
-  let start := info.numParams + 1
-  let stop  := start + info.numDiscrs
-  (simpAppArgRange · start stop)
-    >> tryMatchEquations appFn
-      <|> reduceRecMatcher
-        <| e
-
 def handleConstApp : Simproc := fun e => do
   if (← isCbvOpaque e.getAppFn.constName!) then
     return .rfl (done := true)