From 635a320455d1623f03115fc49649000e330ae7d1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 12 Apr 2021 22:38:15 -0700
Subject: [PATCH] chore: ignore mdata at `intros`

---
 src/Lean/Elab/Tactic/Basic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 9eab27564e..e05790da44 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -454,6 +454,7 @@ where
 private def getIntrosSize : Expr → Nat
   | Expr.forallE _ _ b _ => getIntrosSize b + 1
   | Expr.letE _ _ _ b _  => getIntrosSize b + 1
+  | Expr.mdata _ b _     => getIntrosSize b
   | _                    => 0
 
 /- Recall that `ident' := ident <|> Term.hole` -/