feat: eval new intro "macro"

It is as powerful as the new `fun` term

src/Lean/Elab/Tactic/Basic.lean

@@ -278,11 +278,23 @@ fun stx => do
 @[builtinTactic Lean.Parser.Tactic.assumption] def evalAssumption : Tactic :=
 fun stx => liftMetaTactic $ fun mvarId => do Meta.assumption mvarId; pure []
 
+private def introStep (n : Name) : TacticM Unit :=
+liftMetaTactic $ fun mvarId => do (_, mvarId) ← Meta.intro mvarId n; pure [mvarId]
+
 @[builtinTactic Lean.Parser.Tactic.intro] def evalIntro : Tactic :=
 fun stx => match_syntax stx with
-  | `(tactic| intro)               => liftMetaTactic $ fun mvarId => do (_, mvarId) ← Meta.intro1 mvarId; pure [mvarId]
---   | `(tactic| intro $h) => liftMetaTactic $ fun mvarId => do (_, mvarId) ← Meta.intro mvarId h.getId; pure [mvarId]
-  | _                   => throwUnsupportedSyntax
+  | `(tactic| intro)           => liftMetaTactic $ fun mvarId => do (_, mvarId) ← Meta.intro1 mvarId; pure [mvarId]
+  | `(tactic| intro $h:ident)  => introStep h.getId
+  | `(tactic| intro _)         => introStep `_
+  | `(tactic| intro $pat:term) => do
+    stxNew ← `(tactic| intro h; match h with | $pat:term => _; clear h);
+    withMacroExpansion stx stxNew $ evalTactic stxNew
+  | `(tactic| intro $hs*) => do
+    let h0 := hs.get! 0;
+    let hs := hs.extract 1 hs.size;
+    stxNew ← `(tactic| intro $h0:term; intro $hs*);
+    withMacroExpansion stx stxNew $ evalTactic stxNew
+  | _ => throwUnsupportedSyntax
 
 private def getIntrosSize : Expr → Nat
 | Expr.forallE _ _ b _ => getIntrosSize b + 1

tests/lean/run/intromacro.lean

@@ -0,0 +1,36 @@
+new_frontend
+
+structure S :=
+(x y z : Nat := 0)
+
+def f1 : Nat × Nat → S → Nat :=
+begin
+  intro (x, y);
+  intro ⟨a, b, c⟩;
+  exact x+y+a
+end
+
+theorem ex1 : f1 (10, 20) { x := 10 } = 40 :=
+rfl
+
+def f2 : Nat × Nat → S → Nat :=
+begin
+  intro (a, b) { y := y, .. };
+  exact a+b+y
+end
+
+#eval f2 (10, 20) { y := 5 }
+
+theorem ex2 : f2 (10, 20) { y := 5 } = 35 :=
+rfl
+
+def f3 : Nat × Nat → S → S → Nat :=
+begin
+  intro (a, b) { y := y, .. } s;
+  exact a+b+y+s.x
+end
+
+#eval f3 (10, 20) { y := 5 } { x := 1 }
+
+theorem ex3 : f3 (10, 20) { y := 5 } { x := 1 } = 36 :=
+rfl