feat add evalIntros

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)
 

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