chore: write "|-" as "|" noWs "-" (#2299)

* remove |- as an alias for ⊢

* revert false positive |->

* fix docstring

* undo previous changes

* [unchecked] use suggestion

* next attempt

* add test

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

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

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