From b5fc9c19fe45b6ea72b365b1247fd557b2630683 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 19 Jan 2020 17:48:19 -0800
Subject: [PATCH] feat add `evalIntros`

---
 src/Init/Lean/Elab/Tactic/Basic.lean | 18 ++++++++++++++++++
 tests/lean/run/newfrontend1.lean     | 14 ++++++++++++--
 2 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/src/Init/Lean/Elab/Tactic/Basic.lean b/src/Init/Lean/Elab/Tactic/Basic.lean
index 3fd26191a3..b4844bcc3a 100644
--- a/src/Init/Lean/Elab/Tactic/Basic.lean
+++ b/src/Init/Lean/Elab/Tactic/Basic.lean
@@ -296,6 +296,24 @@ fun stx => match_syntax stx with
   | `(tactic| intro $h) => liftMetaTactic stx $ fun mvarId => do (_, mvarId) ← Meta.intro mvarId h.getId; pure [mvarId]
   | _                   => throwUnsupportedSyntax
 
+private def getIntrosSize : Expr → Nat
+| Expr.forallE _ _ b _ => getIntrosSize b + 1
+| Expr.letE _ _ _ b _  => getIntrosSize b + 1
+| _                    => 0
+
+@[builtinTactic «intros»] def evalIntros : Tactic :=
+fun stx => match_syntax stx with
+  | `(tactic| intros)       => liftMetaTactic stx $ fun mvarId => do
+    type ← Meta.getMVarType mvarId;
+    type ← Meta.instantiateMVars type;
+    let n := getIntrosSize type;
+    (_, mvarId) ← Meta.introN mvarId n;
+    pure [mvarId]
+  | `(tactic| intros $ids*) => liftMetaTactic stx $ fun mvarId => do
+    (_, mvarId) ← Meta.introN mvarId ids.size (ids.map Syntax.getId).toList;
+    pure [mvarId]
+  | _                       => throwUnsupportedSyntax
+
 @[builtinTactic paren] def evalParen : Tactic :=
 fun stx => evalTactic (stx.getArg 1)
 
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index f54a34c438..728e6337a1 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -110,7 +110,8 @@ end
 
 theorem simple9 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 begin
-  intro h1; intro _; intro h3;
+  intros h1 _ h3;
+  traceState;
   { refine Eq.trans ?pre ?post;
     (exact h1) <|> (exact y; exact h3; assumption) }
 end
@@ -151,9 +152,18 @@ end
 
 theorem simple13 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 begin
-  intro h1; intro h2; intro h3;
+  intros h1 h2 h3;
+  traceState;
   apply @Eq.trans;
   case main.b exact y;
   traceState;
   repeat assumption
 end
+
+theorem simple14 (x y z : Nat) : y = z → x = x → x = y → x = z :=
+begin
+  intros;
+  apply @Eq.trans;
+  case main.b exact y;
+  repeat assumption
+end