From 6f71cb1047fea863dbc1cbebc9fad685e4d86a48 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 24 Aug 2021 17:24:29 -0700
Subject: [PATCH] refactor: add `Meta.intros`

---
 src/Lean/Elab/Tactic/BuiltinTactic.lean | 15 +++------------
 src/Lean/Meta/Tactic/Intro.lean         | 12 ++++++++++++
 2 files changed, 15 insertions(+), 12 deletions(-)

diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index ef2111354b..dce1830c2b 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/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 =>
diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean
index c3c1796bbd..4216f4ed9c 100644
--- a/src/Lean/Meta/Tactic/Intro.lean
+++ b/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