refactor: add Meta.intros

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -138,23 +138,14 @@ where
   let stxNew ← liftMacroM <| Term.expandMatchAltsIntoMatchTactic stx matchAlts
   withMacroExpansion stx stxNew <| evalTactic stxNew
 
-private def getIntrosSize : Expr → Nat
-  | Expr.forallE _ _ b _ => getIntrosSize b + 1
-  | Expr.letE _ _ _ b _  => getIntrosSize b + 1
-  | Expr.mdata _ b _     => getIntrosSize b
-  | _                    => 0
-
 @[builtinTactic «intros»] def evalIntros : Tactic := fun stx =>
   match stx with
   | `(tactic| intros) => liftMetaTactic fun mvarId => do
-    let type ← Meta.getMVarType mvarId
-    let type ← instantiateMVars type
-    let n := getIntrosSize type
-    let (_, mvarId) ← Meta.introN mvarId n
-    pure [mvarId]
+    let (_, mvarId) ← Meta.intros mvarId
+    return [mvarId]
   | `(tactic| intros $ids*) => liftMetaTactic fun mvarId => do
     let (_, mvarId) ← Meta.introN mvarId ids.size (ids.map getNameOfIdent').toList
-    pure [mvarId]
+    return [mvarId]
   | _ => throwUnsupportedSyntax
 
 @[builtinTactic Lean.Parser.Tactic.revert] def evalRevert : Tactic := fun stx =>

src/Lean/Meta/Tactic/Intro.lean

@@ -112,4 +112,16 @@ abbrev intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
 abbrev intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   intro1Core mvarId true
 
+private def getIntrosSize : Expr → Nat
+  | Expr.forallE _ _ b _ => getIntrosSize b + 1
+  | Expr.letE _ _ _ b _  => getIntrosSize b + 1
+  | Expr.mdata _ b _     => getIntrosSize b
+  | _                    => 0
+
+def intros (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do
+  let type ← Meta.getMVarType mvarId
+  let type ← instantiateMVars type
+  let n := getIntrosSize type
+  Meta.introN mvarId n
+
 end Lean.Meta