chore: make getIntrosize public

2026-04-16 17:14:08 +00:00 · 2024-10-16 13:15:56 +11:00
1 changed files with 5 additions and 1 deletions
--- a/src/Lean/Meta/Tactic/Intro.lean
+++ b/src/Lean/Meta/Tactic/Intro.lean
@@ -164,7 +164,11 @@ does not start with a forall, lambda or let. -/
 abbrev _root_.Lean.MVarId.intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
  intro1Core mvarId true

-private partial def getIntrosSize : Expr → Nat
+/--
+Calculate the number of new hypotheses that would be created by `intros`,
+i.e. the number of binders which can be introduced without unfolding definitions.
+-/
+partial def getIntrosSize : Expr → Nat
  | .forallE _ _ b _ => getIntrosSize b + 1
  | .letE _ _ _ b _  => getIntrosSize b + 1
  | .mdata _ b       => getIntrosSize b