From 7d39a0d56c3c6f2d5f4b10ea18f9b240dcd045a8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 10 May 2021 16:42:47 -0700
Subject: [PATCH] chore: prepare to change `first` syntax

---
 src/Init/Notation.lean          |  1 +
 src/Lean/Elab/Tactic/Basic.lean | 19 +++++++++++++++++--
 2 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 8ee8da61ac..9f1b49f9a9 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -227,6 +227,7 @@ syntax (name := paren) "(" tacticSeq ")" : tactic
 syntax (name := withReducible) "withReducible " tacticSeq : tactic
 syntax (name := withReducibleAndInstances) "withReducibleAndInstances " tacticSeq : tactic
 syntax (name := first) "first " "|"? sepBy1(tacticSeq, "|") : tactic
+syntax (name := firstNew) "firstNew " withPosition((group(colGe "|" tacticSeq))+) : tactic
 syntax (name := rotateLeft) "rotateLeft" (num)? : tactic
 syntax (name := rotateRight) "rotateRight" (num)? : tactic
 macro "try " t:tacticSeq : tactic => `(first $t | skip)
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 8c7b303f08..d5bcbf4e91 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -622,10 +622,25 @@ def withCaseRef [Monad m] [MonadRef m] (arrow body : Syntax) (x : m α) : m α :
     setGoals gs
   | _ => throwUnsupportedSyntax
 
-@[builtinTactic «first»] partial def evalFirst : Tactic := fun stx => do
-  let tacs := stx[2].getSepArgs
+-- syntax (name := firstNew) "firstNew " withPosition((colGe "|" tacticSeq)+) : tactic
+@[builtinTactic «firstNew»] partial def evalFirstNew : Tactic := fun stx => do
+  let tacs := stx[1].getArgs
   if tacs.isEmpty then throwUnsupportedSyntax
   loop tacs 0
+where
+  loop (tacs : Array Syntax) (i : Nat) :=
+    if i == tacs.size - 1 then
+      evalTactic tacs[i][1]
+    else
+      evalTactic tacs[i][1] <|> loop tacs (i+1)
+
+@[builtinTactic «first»] partial def evalFirst : Tactic := fun stx => do
+  if stx.getNumArgs == 2 then
+    evalFirstNew stx
+  else
+    let tacs := stx[2].getSepArgs
+    if tacs.isEmpty then throwUnsupportedSyntax
+    loop tacs 0
 where
   loop (tacs : Array Syntax) (i : Nat) :=
     if i == tacs.size - 1 then