From bcf5fd866d8cf6123e24b53e4ab64c329a9d0783 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 15 Aug 2024 15:45:54 +0200
Subject: [PATCH] feat: unify equational theorems between wf and structural
 recursion

by removing the `tryRefl` variation between the two.

Part of #3983
---
 src/Lean/Elab/PreDefinition/Eqns.lean            | 6 +-----
 src/Lean/Elab/PreDefinition/Structural/Eqns.lean | 2 +-
 src/Lean/Elab/PreDefinition/WF/Eqns.lean         | 2 +-
 3 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index 3add152548ad..1dc63eedf44c 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -228,16 +228,12 @@ private def shouldUseSimpMatch (e : Expr) : MetaM Bool := do
             throwThe Unit ()
   return (← (find e).run) matches .error _
 
-partial def mkEqnTypes (tryRefl : Bool) (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
+partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
   let (_, eqnTypes) ← go mvarId |>.run { declNames } |>.run #[]
   return eqnTypes
 where
   go (mvarId : MVarId) : ReaderT Context (StateRefT (Array Expr) MetaM) Unit := do
     trace[Elab.definition.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}"
-    if tryRefl then
-      if (← tryURefl mvarId) then
-        saveEqn mvarId
-        return ()
 
     if let some mvarId ← expandRHS? mvarId then
       return (← go mvarId)
diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
index f377b1bd416c..1f0b71753bff 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -64,7 +64,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
-    mkEqnTypes (tryRefl := true) info.declNames goal.mvarId!
+    mkEqnTypes info.declNames goal.mvarId!
   let baseName := info.declName
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do
diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
index abf868cd94d8..41ad8bda2059 100644
--- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
@@ -81,7 +81,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
     let target ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
     withReducible do
-      mkEqnTypes (tryRefl := false) info.declNames goal.mvarId!
+      mkEqnTypes info.declNames goal.mvarId!
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]!