From 80f76d42bd9d73ffbef880d4945f370e040b8097 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 1 Feb 2025 07:44:11 +0100
Subject: [PATCH] Switch to new syntax

---
 src/Init/Control/Basic.lean      | 12 ++---
 src/Init/Core.lean               | 28 +++++-----
 src/Init/Data/Array/Basic.lean   |  4 +-
 src/Init/Data/BitVec/Basic.lean  |  4 +-
 src/Init/Data/Bool.lean          |  2 +-
 src/Init/Data/List/Basic.lean    |  6 +--
 src/Init/Data/List/Notation.lean |  4 +-
 src/Init/Data/Vector/Basic.lean  |  4 +-
 src/Init/GetElem.lean            |  8 +--
 src/Init/Notation.lean           | 90 ++++++++++++++++----------------
 src/Init/NotationExtra.lean      |  2 +-
 src/Lean/Parser/Term.lean        |  2 +-
 12 files changed, 83 insertions(+), 83 deletions(-)

diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean
index dffeddfc9f74..45df7e263973 100644
--- a/src/Init/Control/Basic.lean
+++ b/src/Init/Control/Basic.lean
@@ -50,7 +50,7 @@ def Functor.mapRev {f : Type u → Type v} [Functor f] {α β : Type u} : f α 
 
 infixr:100 " <&> " => Functor.mapRev
 
-recommended_spelling "<&>" "mapRev" Functor.mapRev «term_<&>_»
+recommended_spelling "mapRev" for "<&>" in [Functor.mapRev, «term_<&>_»]
 
 @[always_inline, inline]
 def Functor.discard {f : Type u → Type v} {α : Type u} [Functor f] (x : f α) : f PUnit :=
@@ -122,7 +122,7 @@ instance : ToBool Bool where
 
 infixr:30 " <||> " => orM
 
-recommended_spelling "<||>" "orM" orM «term_<||>_»
+recommended_spelling "orM" for "<||>" in [orM, «term_<||>_»]
 
 @[macro_inline] def andM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
   let b ← x
@@ -132,7 +132,7 @@ recommended_spelling "<||>" "orM" orM «term_<||>_»
 
 infixr:35 " <&&> " => andM
 
-recommended_spelling "<&&>" "andM" andM «term_<&&>_»
+recommended_spelling "andM" for "<&&>" in [andM, «term_<&&>_»]
 
 @[macro_inline] def notM {m : Type → Type v} [Applicative m] (x : m Bool) : m Bool :=
   not <$> x
@@ -322,6 +322,6 @@ def Bind.bindLeft [Bind m] (f : α → m β) (ma : m α) : m β :=
 @[inherit_doc] infixr:55 " <=< " => Bind.kleisliLeft
 @[inherit_doc] infixr:55 " =<< " => Bind.bindLeft
 
-recommended_spelling ">=>" "kleisliRight" Bind.kleisliRight «term_>=>_»
-recommended_spelling "<=<" "kleisliLeft" Bind.kleisliLeft «term_<=<_»
-recommended_spelling "=<<" "bindLeft" Bind.bindLeft «term_=<<_»
+recommended_spelling "kleisliRight" for ">=>" in [Bind.kleisliRight, «term_>=>_»]
+recommended_spelling "kleisliLeft" for "<=<" in [Bind.kleisliLeft, «term_<=<_»]
+recommended_spelling "bindLeft" for "=<<" in [Bind.bindLeft, «term_=<<_»]
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 66aff313cf2c..956ac0900662 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -133,9 +133,9 @@ structure Iff (a b : Prop) : Prop where
 @[inherit_doc] infix:20 " <-> " => Iff
 @[inherit_doc] infix:20 " ↔ "   => Iff
 
-recommended_spelling "↔" "iff" Iff «term_↔_»
+recommended_spelling "iff" for "↔" in [Iff, «term_↔_»]
 /-- prefer `↔` over `<->` -/
-recommended_spelling "<->" "iff" Iff «term_<->_»
+recommended_spelling "iff" for "<->" in [Iff, «term_<->_»]
 
 /--
 `Sum α β`, or `α ⊕ β`, is the disjoint union of types `α` and `β`.
@@ -404,7 +404,7 @@ class HasEquiv (α : Sort u) where
 
 @[inherit_doc] infix:50 " ≈ "  => HasEquiv.Equiv
 
-recommended_spelling "≈" "equiv" HasEquiv.Equiv «term_≈_»
+recommended_spelling "equiv" for "≈" in [HasEquiv.Equiv, «term_≈_»]
 
 /-! # set notation  -/
 
@@ -468,15 +468,15 @@ consisting of all elements in `a` that are not in `b`.
 -/
 infix:70 " \\ " => SDiff.sdiff
 
-recommended_spelling "⊆" "subset" Subset «term_⊆_»
-recommended_spelling "⊂" "ssubset" SSubset «term_⊂_»
+recommended_spelling "subset" for "⊆" in [Subset, «term_⊆_»]
+recommended_spelling "ssubset" for "⊂" in [SSubset, «term_⊂_»]
 /-- prefer `⊆` over `⊇` -/
-recommended_spelling "⊇" "superset" Superset «term_⊇_»
+recommended_spelling "superset" for "⊇" in [Superset, «term_⊇_»]
 /-- prefer `⊂` over `⊃` -/
-recommended_spelling "⊃" "ssuperset" SSuperset «term_⊃_»
-recommended_spelling "∪" "union" Union.union «term_∪_»
-recommended_spelling "∩" "inter" Inter.inter «term_∩_»
-recommended_spelling "\\" "sdiff" SDiff.sdiff «term_\_»
+recommended_spelling "ssuperset" for "⊃" in [SSuperset, «term_⊃_»]
+recommended_spelling "union" for "∪" in [Union.union, «term_∪_»]
+recommended_spelling "inter" for "∩" in [Inter.inter, «term_∩_»]
+recommended_spelling "sdiff" for "\\" in [SDiff.sdiff, «term_\_»]
 
 /-! # collections  -/
 
@@ -489,8 +489,8 @@ class EmptyCollection (α : Type u) where
 @[inherit_doc] notation "{" "}" => EmptyCollection.emptyCollection
 @[inherit_doc] notation "∅"     => EmptyCollection.emptyCollection
 
-recommended_spelling "{}" "empty" EmptyCollection.emptyCollection «term{}»
-recommended_spelling "∅" "empty" EmptyCollection.emptyCollection «term∅»
+recommended_spelling "empty" for "{}" in [EmptyCollection.emptyCollection, «term{}»]
+recommended_spelling "empty" for "∅" in [EmptyCollection.emptyCollection, «term∅»]
 
 /--
 Type class for the `insert` operation.
@@ -669,7 +669,7 @@ Unlike `x ≠ y` (which is notation for `Ne x y`), this is `Bool` valued instead
 
 @[inherit_doc] infix:50 " != " => bne
 
-recommended_spelling "!=" "bne" bne «term_!=_»
+recommended_spelling "bne" for "!=" in [bne, «term_!=_»]
 
 /--
 `LawfulBEq α` is a typeclass which asserts that the `BEq α` implementation
@@ -747,7 +747,7 @@ and asserts that `a` and `b` are not equal.
 
 @[inherit_doc] infix:50 " ≠ "  => Ne
 
-recommended_spelling "≠" "ne" Ne «term_≠_»
+recommended_spelling "ne" for "≠" in [Ne, «term_≠_»]
 
 section Ne
 variable {α : Sort u}
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index ca3d34c12dbd..f656f988a047 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -24,8 +24,8 @@ syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
 macro_rules
   | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
 
-recommended_spelling "#[]" "empty" «term#[_,]»
-recommended_spelling "#[x]" "singleton" «term#[_,]»
+recommended_spelling "empty" for "#[]" in [«term#[_,]»]
+recommended_spelling "singleton" for "#[x]" in [«term#[_,]»]
 
 variable {α : Type u}
 
diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index c5219896d458..451482e76711 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -158,9 +158,9 @@ syntax:max num noWs "#" noWs term:max : term
 macro_rules | `($i:num#$n) => `(BitVec.ofNat $n $i)
 
 /-- not `ofNat_zero` -/
-recommended_spelling "0#n" "zero" BitVec.ofNat «term__#__»
+recommended_spelling "zero" for "0#n" in [BitVec.ofNat, «term__#__»]
 /-- not `ofNat_one` -/
-recommended_spelling "1#n" "one" BitVec.ofNat «term__#__»
+recommended_spelling "one" for "1#n" in [BitVec.ofNat, «term__#__»]
 
 /-- Unexpander for bit vector literals. -/
 @[app_unexpander BitVec.ofNat] def unexpandBitVecOfNat : Lean.PrettyPrinter.Unexpander
diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index 544733fe0e1f..2441c91610af 100644
--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -14,7 +14,7 @@ abbrev xor : Bool → Bool → Bool := bne
 
 @[inherit_doc] infixl:33 " ^^ " => xor
 
-recommended_spelling "^^" "xor" xor «term_^^_»
+recommended_spelling "xor" for "^^" in [xor, «term_^^_»]
 
 instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∀ x, p x) :=
   match inst true, inst false with
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 703ca952a93b..c6d72a21ab4d 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -960,7 +960,7 @@ def IsPrefix (l₁ : List α) (l₂ : List α) : Prop := Exists fun t => l₁ ++
 @[inherit_doc] infixl:50 " <+: " => IsPrefix
 
 /-- not `isPrefix` -/
-recommended_spelling "<+:" "prefix" IsPrefix «term_<+:_»
+recommended_spelling "prefix" for "<+:" in [IsPrefix, «term_<+:_»]
 
 /--  `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`.
 That is, there exists a `t` such that `l₂ == l₁ ++ t`. -/
@@ -1005,7 +1005,7 @@ def IsSuffix (l₁ : List α) (l₂ : List α) : Prop := Exists fun t => t ++ l
 @[inherit_doc] infixl:50 " <:+ " => IsSuffix
 
 /-- not `isSuffix` -/
-recommended_spelling "<:+" "suffix" IsSuffix «term_<:+_»
+recommended_spelling "suffix" for "<:+" in [IsSuffix, «term_<:+_»]
 
 /-! ### IsInfix -/
 
@@ -1018,7 +1018,7 @@ def IsInfix (l₁ : List α) (l₂ : List α) : Prop := Exists fun s => Exists f
 @[inherit_doc] infixl:50 " <:+: " => IsInfix
 
 /-- not `isInfix` -/
-recommended_spelling "<:+:" "infix" IsInfix «term_<:+:_»
+recommended_spelling "infix" for "<:+:" in [IsInfix, «term_<:+:_»]
 
 /-! ### splitAt -/
 
diff --git a/src/Init/Data/List/Notation.lean b/src/Init/Data/List/Notation.lean
index 09e50a919d75..4c3db6cd9e2d 100644
--- a/src/Init/Data/List/Notation.lean
+++ b/src/Init/Data/List/Notation.lean
@@ -26,8 +26,8 @@ unless you use side effecting operations like `dbg_trace`.
 -/
 syntax "[" withoutPosition(term,*,?) "]"  : term
 
-recommended_spelling "[]" "nil" List.nil «term[_]»
-recommended_spelling "[a]" "singleton" List.cons «term[_]»
+recommended_spelling "nil" for "[]" in [List.nil, «term[_]»]
+recommended_spelling "singleton" for "[a]" in [List.cons, «term[_]»]
 
 /--
 Auxiliary syntax for implementing `[$elem,*]` list literal syntax.
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index b93add43ad8b..1f3c8dea0fc2 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -36,8 +36,8 @@ open Lean in
 macro_rules
   | `(#v[ $elems,* ]) => `(Vector.mk (n := $(quote elems.getElems.size)) #[$elems,*] rfl)
 
-recommended_spelling "#v[]" "empty" Vector.mk «term#v[_,]»
-recommended_spelling "#v[x]" "singleton" Vector.mk «term#v[_,]»
+recommended_spelling "empty" for "#v[]" in [Vector.mk, «term#v[_,]»]
+recommended_spelling "singleton" for "#v[x]" in [Vector.mk, «term#v[_,]»]
 
 /-- Custom eliminator for `Vector α n` through `Array α` -/
 @[elab_as_elim]
diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean
index ba5d9f5859cc..817d99cb2a79 100644
--- a/src/Init/GetElem.lean
+++ b/src/Init/GetElem.lean
@@ -114,10 +114,10 @@ panics `i` is out of bounds.
 -/
 macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
 
-recommended_spelling "xs[i]" "getElem" GetElem.getElem «term__[_]»
-recommended_spelling "xs[i]'h" "getElem" GetElem.getElem «term__[_]'_»
-recommended_spelling "xs[i]?" "getElem?" GetElem?.getElem? «term__[_]_?»
-recommended_spelling "xs[i]!" "getElem!" GetElem?.getElem! «term__[_]_!»
+recommended_spelling "getElem" for "xs[i]" in [GetElem.getElem, «term__[_]»]
+recommended_spelling "getElem" for "xs[i]'h" in [GetElem.getElem, «term__[_]'_»]
+recommended_spelling "getElem?" for "xs[i]?" in [GetElem?.getElem?, «term__[_]_?»]
+recommended_spelling "getElem!" for "xs[i]!" in [GetElem?.getElem!, «term__[_]_!»]
 
 instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
     GetElem? coll idx elem valid where
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 72c03d76ece4..debb6d14a3d4 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -273,9 +273,9 @@ syntax (name := rawNatLit) "nat_lit " num : term
 @[inherit_doc] infixr:35 " × "  => Prod
 @[inherit_doc] infixr:35 " ×' " => PProd
 
-recommended_spelling "∘" "comp" Function.comp «term_∘_»
-recommended_spelling "×" "Prod" Prod «term_×_»
-recommended_spelling "×'" "PProd" PProd «term_×'_»
+recommended_spelling "comp" for "∘" in [Function.comp, «term_∘_»]
+recommended_spelling "Prod" for "×" in [Prod, «term_×_»]
+recommended_spelling "PProd" for "×'" in [PProd, «term_×'_»]
 
 @[inherit_doc] infix:50  " ∣ " => Dvd.dvd
 @[inherit_doc] infixl:55 " ||| " => HOr.hOr
@@ -310,23 +310,23 @@ macro_rules | `($x ^ $y)   => `(rightact% HPow.hPow $x $y)
 macro_rules | `($x ++ $y)  => `(binop% HAppend.hAppend $x $y)
 macro_rules | `(- $x)      => `(unop% Neg.neg $x)
 
-recommended_spelling "|||" "or" HOr.hOr «term_|||_»
-recommended_spelling "^^^" "xor" HXor.hXor «term_^^^_»
-recommended_spelling "&&&" "and" HAnd.hAnd «term_&&&_»
-recommended_spelling "+" "add" HAdd.hAdd «term_+_»
+recommended_spelling "or" for "|||" in [HOr.hOr, «term_|||_»]
+recommended_spelling "xor" for "^^^" in [HXor.hXor, «term_^^^_»]
+recommended_spelling "and" for "&&&" in [HAnd.hAnd, «term_&&&_»]
+recommended_spelling "add" for "+" in [HAdd.hAdd, «term_+_»]
 /-- when used as a binary operator -/
-recommended_spelling "-" "sub" HSub.hSub «term_-_»
-recommended_spelling "*" "mul" HMul.hMul «term_*_»
-recommended_spelling "/" "div" HDiv.hDiv «term_/_»
-recommended_spelling "%" "mod" HMod.hMod «term_%_»
-recommended_spelling "^" "pow" HPow.hPow «term_^_»
-recommended_spelling "++" "append" HAppend.hAppend «term_++_»
+recommended_spelling "sub" for "-" in [HSub.hSub, «term_-_»]
+recommended_spelling "mul" for "*" in [HMul.hMul, «term_*_»]
+recommended_spelling "div" for "/" in [HDiv.hDiv, «term_/_»]
+recommended_spelling "mod" for "%" in [HMod.hMod, «term_%_»]
+recommended_spelling "pow" for "^" in [HPow.hPow, «term_^_»]
+recommended_spelling "append" for "++" in [HAppend.hAppend, «term_++_»]
 /-- when used as a unary operator -/
-recommended_spelling "-" "neg" Neg.neg «term-_»
-recommended_spelling "∣" "dvd" Dvd.dvd «term_∣_»
-recommended_spelling "<<<" "shiftLeft" HShiftLeft.hShiftLeft «term_<<<_»
-recommended_spelling ">>>" "shiftRight" HShiftRight.hShiftRight «term_>>>_»
-recommended_spelling "~~~" "not" Complement.complement «term~~~_»
+recommended_spelling "neg" for "-" in [Neg.neg, «term-_»]
+recommended_spelling "dvd" for "∣" in [Dvd.dvd, «term_∣_»]
+recommended_spelling "shiftLeft" for "<<<" in [HShiftLeft.hShiftLeft, «term_<<<_»]
+recommended_spelling "shiftRight" for ">>>" in [HShiftRight.hShiftRight, «term_>>>_»]
+recommended_spelling "not" for "~~~" in [Complement.complement, «term~~~_»]
 
 -- declare ASCII alternatives first so that the latter Unicode unexpander wins
 @[inherit_doc] infix:50 " <= " => LE.le
@@ -352,16 +352,16 @@ macro_rules | `($x ≥ $y)  => `(binrel% GE.ge $x $y)
 macro_rules | `($x = $y)  => `(binrel% Eq $x $y)
 macro_rules | `($x == $y) => `(binrel_no_prop% BEq.beq $x $y)
 
-recommended_spelling "≤" "le" LE.le «term_≤_»
+recommended_spelling "le" for "≤" in [LE.le, «term_≤_»]
 /-- prefer `≤` over `<=` -/
-recommended_spelling "<=" "le" LE.le «term_<=_»
-recommended_spelling "<" "lt" LT.lt «term_<_»
-recommended_spelling ">" "gt" GT.gt «term_>_»
-recommended_spelling "≥" "ge" GE.ge «term_≥_»
+recommended_spelling "le" for "<=" in [LE.le, «term_<=_»]
+recommended_spelling "lt" for "<" in [LT.lt, «term_<_»]
+recommended_spelling "gt" for ">" in [GT.gt, «term_>_»]
+recommended_spelling "ge" for "≥" in [GE.ge, «term_≥_»]
 /-- prefer `≥` over `>=` -/
-recommended_spelling ">=" "ge" GE.ge «term_>=_»
-recommended_spelling "=" "eq" Eq «term_=_»
-recommended_spelling "==" "beq" BEq.beq «term_==_»
+recommended_spelling "ge" for ">=" in [GE.ge, «term_>=_»]
+recommended_spelling "eq" for "=" in [Eq, «term_=_»]
+recommended_spelling "beq" for "==" in [BEq.beq, «term_==_»]
 
 @[inherit_doc] infixr:35 " /\\ " => And
 @[inherit_doc] infixr:35 " ∧ "   => And
@@ -369,28 +369,28 @@ recommended_spelling "==" "beq" BEq.beq «term_==_»
 @[inherit_doc] infixr:30 " ∨  "  => Or
 @[inherit_doc] notation:max "¬" p:40 => Not p
 
-recommended_spelling "∧" "and" And «term_∧_»
+recommended_spelling "and" for "∧" in [And, «term_∧_»]
 /-- prefer `∧` over `/\` -/
-recommended_spelling "/\\" "and" And «term_/\_»
-recommended_spelling "∨" "or" Or «term_∨_»
+recommended_spelling "and" for "/\\" in [And, «term_/\_»]
+recommended_spelling "or" for "∨" in [Or, «term_∨_»]
 /-- prefer `∨` over `\/` -/
-recommended_spelling "\\/" "or" Or «term_\/_»
-recommended_spelling "¬" "not" Not «term¬_»
+recommended_spelling "or" for "\\/" in [Or, «term_\/_»]
+recommended_spelling "not" for "¬" in [Not, «term¬_»]
 
 @[inherit_doc] infixl:35 " && " => and
 @[inherit_doc] infixl:30 " || " => or
 @[inherit_doc] notation:max "!" b:40 => not b
 
-recommended_spelling "&&" "and" and «term_&&_»
-recommended_spelling "||" "or" and «term_||_»
-recommended_spelling "!" "not" not «term!_»
+recommended_spelling "and" for "&&" in [and, «term_&&_»]
+recommended_spelling "or" for "||" in [and, «term_||_»]
+recommended_spelling "not" for "!" in [not, «term!_»]
 
 @[inherit_doc] notation:50 a:50 " ∈ " b:50 => Membership.mem b a
 /-- `a ∉ b` is negated elementhood. It is notation for `¬ (a ∈ b)`. -/
 notation:50 a:50 " ∉ " b:50 => ¬ (a ∈ b)
 
-recommended_spelling "∈" "mem" Membership.mem «term_∈_»
-recommended_spelling "∉" "not_mem" «term_∉_»
+recommended_spelling "mem" for "∈" in [Membership.mem, «term_∈_»]
+recommended_spelling "not_mem" for "∉" in [«term_∉_»]
 
 @[inherit_doc] infixr:67 " :: " => List.cons
 @[inherit_doc] infixr:100 " <$> " => Functor.map
@@ -407,14 +407,14 @@ macro_rules | `($x <*> $y) => `(Seq.seq $x fun _ : Unit => $y)
 macro_rules | `($x <* $y)  => `(SeqLeft.seqLeft $x fun _ : Unit => $y)
 macro_rules | `($x *> $y)  => `(SeqRight.seqRight $x fun _ : Unit => $y)
 
-recommended_spelling "::" "cons" List.cons «term_::_»
-recommended_spelling "<$>" "map" Functor.map «term_<$>_»
-recommended_spelling ">>=" "bind" Bind.bind «term_>>=_»
-recommended_spelling "<|>" "orElse" HOrElse.hOrElse «term_<|>_»
-recommended_spelling ">>" "andThen" HAndThen.hAndThen «term_>>_»
-recommended_spelling "<*>" "seq" Seq.seq «term_<*>_»
-recommended_spelling "<*" "seqLeft" SeqLeft.seqLeft «term_<*_»
-recommended_spelling "*>" "seqRight" SeqRight.seqRight «term_*>_»
+recommended_spelling "cons" for "::" in [List.cons, «term_::_»]
+recommended_spelling "map" for "<$>" in [Functor.map, «term_<$>_»]
+recommended_spelling "bind" for ">>=" in [Bind.bind, «term_>>=_»]
+recommended_spelling "orElse" for "<|>" in [HOrElse.hOrElse, «term_<|>_»]
+recommended_spelling "andThen" for ">>" in [HAndThen.hAndThen, «term_>>_»]
+recommended_spelling "seq" for "<*>" in [Seq.seq, «term_<*>_»]
+recommended_spelling "seqLeft" for "<*" in [SeqLeft.seqLeft, «term_<*_»]
+recommended_spelling "seqRight" for "*>" in [SeqRight.seqRight, «term_*>_»]
 
 namespace Lean
 
@@ -520,7 +520,7 @@ macro_rules
   | `({ $x : $type // $p }) => ``(Subtype (fun ($x:ident : $type) => $p))
   | `({ $x // $p })         => ``(Subtype (fun ($x:ident : _) => $p))
 
-recommended_spelling "{ x // p x }" "subtype" Subtype «term{_:_//_}»
+recommended_spelling "subtype" for "{ x // p x }" in [Subtype, «term{_:_//_}»]
 
 /--
 `without_expected_type t` instructs Lean to elaborate `t` without an expected type.
diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 413701e7d840..0d3b6b036ae6 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -352,7 +352,7 @@ macro_rules
   | `({$x:term}) => `(singleton $x)
   | `({$x:term, $xs:term,*}) => `(insert $x {$xs:term,*})
 
-recommended_spelling "{x}" "singleton" singleton «term{_}»
+recommended_spelling "singleton" for "{x}" in [singleton, «term{_}»]
 
 namespace Lean
 
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 036990ba6c1e..574d1834a442 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -253,7 +253,7 @@ do not yield the right result.
 @[builtin_term_parser] def tuple := leading_parser
   "(" >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", " (allowTrailingSep := true)))) >> ")"
 
-recommended_spelling "(a, b)" "mk" Prod.mk tuple
+recommended_spelling "mk" for "(a, b)" in [Prod.mk, tuple]
 
 /--
 Parentheses, used for grouping expressions (e.g., `a * (b + c)`).