Use isBRecOnRecursor

Author: nomeata

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -50,7 +50,7 @@ where
       unless brecOn.isConst do
         throwError "goal not headed by `.brecOn`\n{MessageData.ofGoal mvarId}"
       let brecOnName := brecOn.constName!
-      unless Name.isSuffixOf `brecOn brecOnName do
+      unless isBRecOnRecursor (← getEnv) brecOnName do
         throwError "goal not headed by `.brecOn`\n{MessageData.ofGoal mvarId}"
       let brecOnThmName := brecOnName.str "eq"
       unless (← hasConst brecOnThmName) do

tests/lean/run/structuralEqns5.lean

@@ -20,26 +20,11 @@ info: theorem Tree.size.eq_def.{u_1} : ∀ {α : Type u_1} (x : Tree α),
 #print sig Tree.size.eq_def
 
 /--
-error: Failed to realize constant Tree.size_aux.eq_def:
-  failed to generate equational theorem for `Tree.size_aux`
-    goal not headed by `.brecOn`
-    α : Type u_1
-    x✝ : List (Tree α)
-    ⊢ (Tree.brecOn_1 x✝
-          (fun x f =>
-            (match (motive := (x : Tree α) → x.below → Nat) x with
-              | Tree.node a tsf => fun x => 1 + (x true).1 + (x false).1)
-              f)
-          fun x f =>
-          (match (motive := (x : List (Tree α)) → Tree.below_1 x → Nat) x with
-            | [] => fun x => 0
-            | t :: ts => fun x => x.1.1 + x.2.1)
-            f) =
-        match x✝ with
-        | [] => 0
-        | t :: ts => t.size + Tree.size_aux ts
----
-error: Unknown constant `Tree.size_aux.eq_def`
+info: theorem Tree.size_aux.eq_def.{u_1} : ∀ {α : Type u_1} (x : List (Tree α)),
+  Tree.size_aux x =
+    match x with
+    | [] => 0
+    | t :: ts => t.size + Tree.size_aux ts
 -/
 #guard_msgs in
 #print sig Tree.size_aux.eq_def