doc: add recommended spellings for many term notations (#6886)

This PR adds recommended spellings for many notations defined in Lean
core, using the `recommended_spelling` command from #6869.

src/Init/Control/Basic.lean

@@ -50,6 +50,8 @@ def Functor.mapRev {f : Type u → Type v} [Functor f] {α β : Type u} : f α 
 
 infixr:100 " <&> " => Functor.mapRev
 
+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 :=
   Functor.mapConst PUnit.unit x
@@ -120,6 +122,8 @@ instance : ToBool Bool where
 
 infixr:30 " <||> " => orM
 
+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
   match toBool b with
@@ -128,6 +132,8 @@ infixr:30 " <||> " => orM
 
 infixr:35 " <&&> " => andM
 
+recommended_spelling "andM" for "<&&>" in [andM, «term_<&&>_»]
+
 @[macro_inline] def notM {m : Type → Type v} [Applicative m] (x : m Bool) : m Bool :=
   not <$> x
 
@@ -315,3 +321,7 @@ def Bind.bindLeft [Bind m] (f : α → m β) (ma : m α) : m β :=
 @[inherit_doc] infixr:55 " >=> " => Bind.kleisliRight
 @[inherit_doc] infixr:55 " <=< " => Bind.kleisliLeft
 @[inherit_doc] infixr:55 " =<< " => Bind.bindLeft
+
+recommended_spelling "kleisliRight" for ">=>" in [Bind.kleisliRight, «term_>=>_»]
+recommended_spelling "kleisliLeft" for "<=<" in [Bind.kleisliLeft, «term_<=<_»]
+recommended_spelling "bindLeft" for "=<<" in [Bind.bindLeft, «term_=<<_»]

src/Init/Core.lean

@@ -133,6 +133,10 @@ structure Iff (a b : Prop) : Prop where
 @[inherit_doc] infix:20 " <-> " => Iff
 @[inherit_doc] infix:20 " ↔ "   => Iff
 
+recommended_spelling "iff" for "↔" in [Iff, «term_↔_»]
+/-- prefer `↔` over `<->` -/
+recommended_spelling "iff" for "<->" in [Iff, «term_<->_»]
+
 /--
 `Sum α β`, or `α ⊕ β`, is the disjoint union of types `α` and `β`.
 An element of `α ⊕ β` is either of the form `.inl a` where `a : α`,
@@ -400,6 +404,8 @@ class HasEquiv (α : Sort u) where
 
 @[inherit_doc] infix:50 " ≈ "  => HasEquiv.Equiv
 
+recommended_spelling "equiv" for "≈" in [HasEquiv.Equiv, «term_≈_»]
+
 /-! # set notation  -/
 
 /-- Notation type class for the subset relation `⊆`. -/
@@ -462,6 +468,16 @@ consisting of all elements in `a` that are not in `b`.
 -/
 infix:70 " \\ " => SDiff.sdiff
 
+recommended_spelling "subset" for "⊆" in [Subset, «term_⊆_»]
+recommended_spelling "ssubset" for "⊂" in [SSubset, «term_⊂_»]
+/-- prefer `⊆` over `⊇` -/
+recommended_spelling "superset" for "⊇" in [Superset, «term_⊇_»]
+/-- prefer `⊂` over `⊃` -/
+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  -/
 
 /-- `EmptyCollection α` is the typeclass which supports the notation `∅`, also written as `{}`. -/
@@ -473,6 +489,9 @@ class EmptyCollection (α : Type u) where
 @[inherit_doc] notation "{" "}" => EmptyCollection.emptyCollection
 @[inherit_doc] notation "∅"     => EmptyCollection.emptyCollection
 
+recommended_spelling "empty" for "{}" in [EmptyCollection.emptyCollection, «term{}»]
+recommended_spelling "empty" for "∅" in [EmptyCollection.emptyCollection, «term∅»]
+
 /--
 Type class for the `insert` operation.
 Used to implement the `{ a, b, c }` syntax.
@@ -650,6 +669,8 @@ Unlike `x ≠ y` (which is notation for `Ne x y`), this is `Bool` valued instead
 
 @[inherit_doc] infix:50 " != " => bne
 
+recommended_spelling "bne" for "!=" in [bne, «term_!=_»]
+
 /--
 `LawfulBEq α` is a typeclass which asserts that the `BEq α` implementation
 (which supplies the `a == b` notation) coincides with logical equality `a = b`.
@@ -726,6 +747,8 @@ and asserts that `a` and `b` are not equal.
 
 @[inherit_doc] infix:50 " ≠ "  => Ne
 
+recommended_spelling "ne" for "≠" in [Ne, «term_≠_»]
+
 section Ne
 variable {α : Sort u}
 variable {a b : α} {p : Prop}

src/Init/Data/Array/Basic.lean

@@ -18,11 +18,15 @@ universe u v w
 
 /-! ### Array literal syntax -/
 
+/-- Syntax for `Array α`. -/
 syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
 
 macro_rules
   | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
 
+recommended_spelling "empty" for "#[]" in [«term#[_,]»]
+recommended_spelling "singleton" for "#[x]" in [«term#[_,]»]
+
 variable {α : Type u}
 
 namespace Array

src/Init/Data/BitVec/Basic.lean

@@ -157,6 +157,11 @@ section Syntax
 syntax:max num noWs "#" noWs term:max : term
 macro_rules | `($i:num#$n) => `(BitVec.ofNat $n $i)
 
+/-- not `ofNat_zero` -/
+recommended_spelling "zero" for "0#n" in [BitVec.ofNat, «term__#__»]
+/-- not `ofNat_one` -/
+recommended_spelling "one" for "1#n" in [BitVec.ofNat, «term__#__»]
+
 /-- Unexpander for bit vector literals. -/
 @[app_unexpander BitVec.ofNat] def unexpandBitVecOfNat : Lean.PrettyPrinter.Unexpander
   | `($(_) $n $i:num) => `($i:num#$n)

src/Init/Data/Bool.lean

@@ -14,6 +14,8 @@ abbrev xor : Bool → Bool → Bool := bne
 
 @[inherit_doc] infixl:33 " ^^ " => xor
 
+recommended_spelling "xor" for "^^" in [xor, «term_^^_»]
+
 instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∀ x, p x) :=
   match inst true, inst false with
   | isFalse ht, _ => isFalse fun h => absurd (h _) ht

src/Init/Data/List/Basic.lean

@@ -959,6 +959,9 @@ def IsPrefix (l₁ : List α) (l₂ : List α) : Prop := Exists fun t => l₁ ++
 
 @[inherit_doc] infixl:50 " <+: " => IsPrefix
 
+/-- not `isPrefix` -/
+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`. -/
 def isPrefixOf [BEq α] : List α → List α → Bool
@@ -1001,6 +1004,9 @@ def IsSuffix (l₁ : List α) (l₂ : List α) : Prop := Exists fun t => t ++ l
 
 @[inherit_doc] infixl:50 " <:+ " => IsSuffix
 
+/-- not `isSuffix` -/
+recommended_spelling "suffix" for "<:+" in [IsSuffix, «term_<:+_»]
+
 /-! ### IsInfix -/
 
 /--
@@ -1011,6 +1017,9 @@ def IsInfix (l₁ : List α) (l₂ : List α) : Prop := Exists fun s => Exists f
 
 @[inherit_doc] infixl:50 " <:+: " => IsInfix
 
+/-- not `isInfix` -/
+recommended_spelling "infix" for "<:+:" in [IsInfix, «term_<:+:_»]
+
 /-! ### splitAt -/
 
 /--

src/Init/Data/List/Notation.lean

@@ -26,6 +26,9 @@ unless you use side effecting operations like `dbg_trace`.
 -/
 syntax "[" withoutPosition(term,*,?) "]"  : 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.
 The syntax `%[a,b,c|tail]` constructs a value equivalent to `a::b::c::tail`.

src/Init/Data/Vector/Basic.lean

@@ -36,6 +36,9 @@ open Lean in
 macro_rules
   | `(#v[ $elems,* ]) => `(Vector.mk (n := $(quote elems.getElems.size)) #[$elems,*] rfl)
 
+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]
 def elimAsArray {motive : Vector α n → Sort u}

src/Init/GetElem.lean

@@ -114,6 +114,11 @@ panics `i` is out of bounds.
 -/
 macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
 
+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
   getElem? xs i := decidableGetElem? xs i

src/Init/Notation.lean

@@ -273,6 +273,10 @@ syntax (name := rawNatLit) "nat_lit " num : term
 @[inherit_doc] infixr:35 " × "  => Prod
 @[inherit_doc] infixr:35 " ×' " => PProd
 
+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
 @[inherit_doc] infixl:58 " ^^^ " => HXor.hXor
@@ -306,6 +310,24 @@ 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" 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" 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" 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
 @[inherit_doc] infix:50 " ≤ "  => LE.le
@@ -330,20 +352,46 @@ 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" for "≤" in [LE.le, «term_≤_»]
+/-- prefer `≤` over `<=` -/
+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" 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
 @[inherit_doc] infixr:30 " \\/ " => Or
 @[inherit_doc] infixr:30 " ∨  "  => Or
 @[inherit_doc] notation:max "¬" p:40 => Not p
 
+recommended_spelling "and" for "∧" in [And, «term_∧_»]
+/-- prefer `∧` over `/\` -/
+recommended_spelling "and" for "/\\" in [And, «term_/\_»]
+recommended_spelling "or" for "∨" in [Or, «term_∨_»]
+/-- prefer `∨` over `\/` -/
+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" 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" for "∈" in [Membership.mem, «term_∈_»]
+recommended_spelling "not_mem" for "∉" in [«term_∉_»]
+
 @[inherit_doc] infixr:67 " :: " => List.cons
 @[inherit_doc] infixr:100 " <$> " => Functor.map
 @[inherit_doc] infixl:55  " >>= " => Bind.bind
@@ -359,6 +407,15 @@ 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" 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
 
 /--
@@ -463,6 +520,8 @@ macro_rules
   | `({ $x : $type // $p }) => ``(Subtype (fun ($x:ident : $type) => $p))
   | `({ $x // $p })         => ``(Subtype (fun ($x:ident : _) => $p))
 
+recommended_spelling "subtype" for "{ x // p x }" in [Subtype, «term{_:_//_}»]
+
 /--
 `without_expected_type t` instructs Lean to elaborate `t` without an expected type.
 Recall that terms such as `match ... with ...` and `⟨...⟩` will postpone elaboration until

src/Init/NotationExtra.lean

@@ -345,12 +345,15 @@ macro:50 e:term:51 " matches " p:sepBy1(term:51, " | ") : term =>
 
 end Lean
 
+/-- `{ a, b, c }` syntax, powered by the `Singleton` and `Insert` typeclasses. -/
 syntax "{" term,+ "}" : term
 
 macro_rules
   | `({$x:term}) => `(singleton $x)
   | `({$x:term, $xs:term,*}) => `(insert $x {$xs:term,*})
 
+recommended_spelling "singleton" for "{x}" in [singleton, «term{_}»]
+
 namespace Lean
 
 /-- Unexpander for the `{ x }` notation. -/

src/Lean/Parser/Term.lean

@@ -254,6 +254,8 @@ do not yield the right result.
 @[builtin_term_parser] def tuple := leading_parser
   "(" >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", " (allowTrailingSep := true)))) >> ")"
 
+recommended_spelling "mk" for "(a, b)" in [Prod.mk, tuple]
+
 /--
 Parentheses, used for grouping expressions (e.g., `a * (b + c)`).
 Can also be used for creating simple functions when combined with `·`. Here are some examples:

tests/lean/interactive/hover.lean.expected.out

@@ -407,7 +407,7 @@
   "end": {"line": 206, "character": 13}},
  "contents":
  {"value":
-  "```lean\n?m x1✝ x2✝\n```\n***\n`a + b` computes the sum of `a` and `b`.\nThe meaning of this notation is type-dependent. ",
+  "```lean\n?m x1✝ x2✝\n```\n***\n`a + b` computes the sum of `a` and `b`.\nThe meaning of this notation is type-dependent. \n\nConventions for notations in identifiers:\n\n * The recommended spelling of `+` in identifiers is `add`.",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 215, "character": 28}}
@@ -612,7 +612,7 @@
   "end": {"line": 290, "character": 16}},
  "contents":
  {"value":
-  "```lean\nList.nil.{u} {α : Type u} : List α\n```\n***\n`[]` is the empty list. \n***\n*import Init.Prelude*",
+  "```lean\nList.nil.{u} {α : Type u} : List α\n```\n***\n`[]` is the empty list. \n\nConventions for notations in identifiers:\n\n * The recommended spelling of `[]` in identifiers is `nil`.\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 292, "character": 13}}
@@ -621,7 +621,7 @@
   "end": {"line": 292, "character": 15}},
  "contents":
  {"value":
-  "```lean\nList.cons.{u} {α : Type u} (head : α) (tail : List α) : List α\n```\n***\nIf `a : α` and `l : List α`, then `cons a l`, or `a :: l`, is the\nlist whose first element is `a` and with `l` as the rest of the list. \n***\n*import Init.Prelude*",
+  "```lean\nList.cons.{u} {α : Type u} (head : α) (tail : List α) : List α\n```\n***\nIf `a : α` and `l : List α`, then `cons a l`, or `a :: l`, is the\nlist whose first element is `a` and with `l` as the rest of the list. \n\nConventions for notations in identifiers:\n\n * The recommended spelling of `::` in identifiers is `cons`.\n\n * The recommended spelling of `[a]` in identifiers is `singleton`.\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 294, "character": 18}}

tests/lean/run/recommendedSpelling.lean

@@ -2,11 +2,10 @@ import Lean
 
 /-!
 Test the `recommended_spelling` command.
-
-TODO: once we use this command in Init, we can test that recommended spellings from imported
-modules are reported correctly.
 -/
 
+recommended_spelling "bland" for "🥤" in [And]
+
 /--
 Conjuction
 
@@ -56,6 +55,13 @@ info: some
 #guard_msgs in
 #eval findDocString? `«term_☋_»
 
+/--
+info: some
+  "`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be\nconstructed and destructed like a pair: if `ha : a` and `hb : b` then\n`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.\n\n\nConventions for notations in identifiers:\n\n * The recommended spelling of `∧` in identifiers is `and`.\n\n * The recommended spelling of `/\\` in identifiers is `and` (prefer `∧` over `/\\`).\n\n * The recommended spelling of `🥤` in identifiers is `bland`."
+-/
+#guard_msgs in
+#eval findDocString? `And
+
 /-- info: 1 -/
 #guard_msgs in
 #eval do