From d8d7d63830538ffb7564c19dd819b732f91ccb63 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 6 Jan 2022 12:24:40 -0800
Subject: [PATCH] fix: registers eqns info before adding definition

Otherwise `[simp]` at definition will fail to generate equational theorems.
---
 src/Lean/Elab/PreDefinition/Structural/Main.lean |  2 +-
 tests/lean/run/simpAtDefIssue.lean               | 11 +++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/simpAtDefIssue.lean

diff --git a/src/Lean/Elab/PreDefinition/Structural/Main.lean b/src/Lean/Elab/PreDefinition/Structural/Main.lean
index 1ef5fdd13a..6379398d1a 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Main.lean
@@ -84,10 +84,10 @@ def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
     let preDefNonRec ← eraseRecAppSyntax preDefNonRec
     let preDef ← eraseRecAppSyntax preDefs[0]
     state.addMatchers.forM liftM
+    registerEqnsInfo preDef recArgPos
     mapError (addNonRec preDefNonRec) (fun msg => m!"structural recursion failed, produced type incorrect term{indentD msg}")
     addAndCompilePartialRec #[preDef]
     addSmartUnfoldingDef preDef recArgPos
-    registerEqnsInfo preDef recArgPos
 
 builtin_initialize
   registerTraceClass `Elab.definition.structural
diff --git a/tests/lean/run/simpAtDefIssue.lean b/tests/lean/run/simpAtDefIssue.lean
new file mode 100644
index 0000000000..e82f81f901
--- /dev/null
+++ b/tests/lean/run/simpAtDefIssue.lean
@@ -0,0 +1,11 @@
+@[simp] def g (x y : Nat) : Nat :=
+  match x, y with
+  | 0,   0 => 1
+  | 0,   y => y
+  | x+1, 5 => 2 * g x 0
+  | x+1, y => 2 * g x y
+
+#check g._eq_1
+#check g._eq_2
+#check g._eq_3
+#check g._eq_4