From aca1d54514913df86652bf4c072b8a7a380bad1c Mon Sep 17 00:00:00 2001
From: jrr6 <7482866+jrr6@users.noreply.github.com>
Date: Mon, 10 Mar 2025 17:18:00 -0400
Subject: [PATCH] refactor: add definitions to allow turnstiles anywhere in
 locations (#7425)

This PR adds definitions that will be required to allow to appear
turnstiles anywhere in tactic location specifiers.

This is the first (pre-stage0 update) half of #6992.
---
 src/Init/Tactics.lean              | 5 +++++
 src/Lean/Elab/Tactic/Location.lean | 9 ++++++++-
 src/stdlib_flags.h                 | 2 ++
 3 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index d9b4983704..841eeb261c 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -461,10 +461,15 @@ syntax config := atomic(" (" &"config") " := " withoutPosition(term) ")"
 /-- The `*` location refers to all hypotheses and the goal. -/
 syntax locationWildcard := " *"
 
+/-- The `⊢` location refers to the current goal. -/
+syntax locationType := patternIgnore(atomic("|" noWs "-") <|> "⊢")
+
 /--
 A hypothesis location specification consists of 1 or more hypothesis references
 and optionally `⊢` denoting the goal.
 -/
+-- Forthcoming definition after stage0 update:
+-- syntax locationHyp := (ppSpace colGt (term:max <|> locationType))+
 syntax locationHyp := (ppSpace colGt term:max)+ patternIgnore(ppSpace (atomic("|" noWs "-") <|> "⊢"))?
 
 /--
diff --git a/src/Lean/Elab/Tactic/Location.lean b/src/Lean/Elab/Tactic/Location.lean
index 9e4da6dd61..1144830b91 100644
--- a/src/Lean/Elab/Tactic/Location.lean
+++ b/src/Lean/Elab/Tactic/Location.lean
@@ -30,7 +30,14 @@ def expandLocation (stx : Syntax) : Location :=
   if arg.getKind == ``Parser.Tactic.locationWildcard then
     Location.wildcard
   else
-    Location.targets arg[0].getArgs (!arg[1].isNone)
+    -- Temporary workaround to accommodate stage0 update
+    if arg[1] matches .missing then
+      let locationHyps := arg[0].getArgs
+      let hypotheses := locationHyps.filter (·.getKind != ``Parser.Tactic.locationType)
+      let numTurnstiles := locationHyps.size - hypotheses.size
+      Location.targets hypotheses (numTurnstiles > 0)
+    else
+      Location.targets arg[0].getArgs (!arg[1].isNone)
 
 def expandOptLocation (stx : Syntax) : Location :=
   if stx.isNone then
diff --git a/src/stdlib_flags.h b/src/stdlib_flags.h
index b647d85f37..ee225c1734 100644
--- a/src/stdlib_flags.h
+++ b/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;