From 1a6663a41baf95cb995b79cd8a466ab81e230b35 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Fri, 14 Jul 2023 18:48:20 +0200
Subject: [PATCH] chore: write `"|-"` as `"|" noWs "-"` (#2299)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* remove |- as an alias for ⊢

* revert false positive |->

* fix docstring

* undo previous changes

* [unchecked] use suggestion

* next attempt

* add test
---
 src/Init/NotationExtra.lean | 2 +-
 src/Init/Tactics.lean       | 2 +-
 tests/lean/run/2299.lean    | 7 +++++++
 3 files changed, 9 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/2299.lean

diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 1b7a8296e8..016ba7d734 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -65,7 +65,7 @@ syntax unifConstraint := term patternIgnore(" =?= " <|> " ≟ ") term
 syntax unifConstraintElem := colGe unifConstraint ", "?
 
 syntax (docComment)? attrKind "unif_hint" (ppSpace ident)? (ppSpace bracketedBinder)*
-  " where " withPosition(unifConstraintElem*) patternIgnore("|-" <|> "⊢ ") unifConstraint : command
+  " where " withPosition(unifConstraintElem*) patternIgnore(atomic("|" noWs "-") <|> "⊢") unifConstraint : command
 
 macro_rules
   | `($[$doc?:docComment]? $kind:attrKind unif_hint $(n)? $bs* where $[$cs₁ ≟ $cs₂]* |- $t₁ ≟ $t₂) => do
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 845a824773..a5c9981ece 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -304,7 +304,7 @@ syntax locationWildcard := " *"
 A hypothesis location specification consists of 1 or more hypothesis references
 and optionally `⊢` denoting the goal.
 -/
-syntax locationHyp := (ppSpace colGt term:max)+ ppSpace patternIgnore("⊢" <|> "|-")?
+syntax locationHyp := (ppSpace colGt term:max)+ ppSpace patternIgnore( atomic("|" noWs "-") <|> "⊢")?
 
 /--
 Location specifications are used by many tactics that can operate on either the
diff --git a/tests/lean/run/2299.lean b/tests/lean/run/2299.lean
new file mode 100644
index 0000000000..9a6c372bfc
--- /dev/null
+++ b/tests/lean/run/2299.lean
@@ -0,0 +1,7 @@
+class Abs (α : Type _) where
+  abs : α → α
+
+macro:max atomic("|" noWs) a:term noWs "|" : term => `(Abs.abs $a)
+
+-- check that `|-` is not parsed as a single token.
+example [Abs α] [Neg α] (n : α) : |-n| = |-n| := rfl