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