From 7df9cf6a0aedea9b80ff3f10e3291f9ab0166e83 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Dec 2021 07:15:14 -0800
Subject: [PATCH] feat: eliminate "recAppSyntax" information during structural
 recursion

---
 src/Lean/Elab/PreDefinition/Structural/BRecOn.lean | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
index 39479ff6be..dbd98408d8 100644
--- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Meta.Match.Match
+import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Structural.Basic
 
 namespace Lean.Elab.Structural
@@ -91,7 +92,11 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
     | Expr.letE n type val body _ =>
       withLetDecl n (← loop below type) (← loop below val) fun x => do
         mkLetFVars #[x] (← loop below (body.instantiate1 x)) (usedLetOnly := false)
-    | Expr.mdata d e _   => return mkMData d (← loop below e)
+    | Expr.mdata d b _   =>
+      if let some stx := getRecAppSyntax? e then
+        loop below b
+      else
+        return mkMData d (← loop below b)
     | Expr.proj n i e _  => return mkProj n i (← loop below e)
     | Expr.app _ _ _ =>
       let processApp (e : Expr) : M Expr :=