feat: add evalChoice

cc @Kha

src/Init/Lean/Elab/Tactic/Basic.lean

@@ -297,6 +297,21 @@ match newGoals with
 @[builtinTactic seq] def evalSeq : Tactic :=
 fun stx => (stx.getArg 0).forSepArgsM evalTactic
 
+partial def evalChoiceAux (tactics : Array Syntax) : Nat → TacticM Unit
+| i =>
+  if h : i < tactics.size then
+    let tactic := tactics.get ⟨i, h⟩;
+    catch
+      (evalTactic tactic)
+      (fun ex => match ex with
+        | Exception.unsupportedSyntax => evalChoiceAux (i+1)
+        | _ => throw ex)
+  else
+    throwUnsupportedSyntax
+
+@[builtinTactic choice] def evalChoice : Tactic :=
+fun stx => evalChoiceAux stx.getArgs 0
+
 @[builtinTactic skip] def evalSkip : Tactic :=
 fun stx => pure ()
 

tests/lean/run/tacticExtOverlap.lean

@@ -0,0 +1,27 @@
+new_frontend
+
+open Lean
+
+syntax [myintro] "intros" (sepBy ident ",") : tactic
+
+macro_rules [myintro]
+| `(tactic| intros $x*) => pure $ Syntax.node `Lean.Parser.Tactic.intros #[Syntax.atom none "intros", mkNullNode x.getSepElems]
+
+theorem tst1 {p q : Prop} : p → q → p :=
+begin
+  intros h1, h2;
+  assumption
+end
+
+theorem tst2 {p q : Prop} : p → q → p :=
+begin
+  intros h1; -- the builtin and myintro overlap here.
+  intros h2; -- the builtin and myintro overlap here.
+  assumption
+end
+
+theorem tst3 {p q : Prop} : p → q → p :=
+begin
+  intros h1 h2;
+  assumption
+end