From 2ae78a474ddf0a39bc2afb9f9f284d2e64f48a70 Mon Sep 17 00:00:00 2001
From: Jannis Limperg <jannis@limperg.de>
Date: Tue, 9 Jan 2024 16:01:56 +0100
Subject: [PATCH] BuiltinRules.Intros: use getIntrosSize from core

We now use the (private) function `getIntrosSize` from core instead of
copy-pasting it. This should future-proof Aesop for the changes in
leanprover/lean4#3115.
---
 Aesop/BuiltinRules/Intros.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/Aesop/BuiltinRules/Intros.lean b/Aesop/BuiltinRules/Intros.lean
index 2ca1db98..e306f637 100644
--- a/Aesop/BuiltinRules/Intros.lean
+++ b/Aesop/BuiltinRules/Intros.lean
@@ -5,17 +5,14 @@ Authors: Jannis Limperg, Kyle Miller
 -/
 
 import Aesop.Frontend.Attribute
+import Std.Tactic.OpenPrivate
 
 open Lean
 open Lean.Meta
 
 namespace Aesop.BuiltinRules
 
-private def getIntrosSize : Expr → Nat
-  | .forallE _ _ b _ => getIntrosSize b + 1
-  | .letE _ _ _ b _  => getIntrosSize b + 1
-  | .mdata _ b       => getIntrosSize b
-  | _                => 0
+open private getIntrosSize in Lean.MVarId.intros
 
 /-- Introduce as many binders as possible while unfolding definitions with the
 ambient transparency. -/