Get started

src/Init/Core.lean

@@ -644,6 +644,8 @@ the `BEq` typeclass.
 
 Unlike `x ≠ y` (which is notation for `Ne x y`), this is `Bool` valued instead of
 `Prop` valued. It is mainly intended for programming applications.
+
+The recommended way to refer to this notation in names is `bne`.
 -/
 @[inline] def bne {α : Type u} [BEq α] (a b : α) : Bool :=
   !(a == b)

src/Init/Data/BitVec/Basic.lean

@@ -153,7 +153,10 @@ end Int
 
 section Syntax
 
-/-- Notation for bit vector literals. `i#n` is a shorthand for `BitVec.ofNat n i`. -/
+/-- Notation for bit vector literals. `i#n` is a shorthand for `BitVec.ofNat n i`.
+
+The recommended way to refer to this notation in names is to suppress it, i.e., `0#n` should turn
+into `zero`, not `ofNat_zero`. -/
 syntax:max num noWs "#" noWs term:max : term
 macro_rules | `($i:num#$n) => `(BitVec.ofNat $n $i)
 

src/Init/Data/Vector/Basic.lean

@@ -28,7 +28,11 @@ abbrev Array.toVector (xs : Array α) : Vector α xs.size := .mk xs rfl
 
 namespace Vector
 
-/-- Syntax for `Vector α n` -/
+/-- Syntax for `Vector α n`
+
+The recommended way to refer to `#v[]` in names is `empty`.
+
+The recommended way to refer to `#v[a]` in names is `singleton`. -/
 syntax "#v[" withoutPosition(sepBy(term, ", ")) "]" : term
 
 open Lean in

src/Init/Prelude.lean

@@ -1037,6 +1037,8 @@ if `x` is false then `y` is not evaluated.
 /--
 `not x`, or `!x`, is the boolean "not" operation (not to be confused
 with `Not : Prop → Prop`, which is the propositional connective).
+
+The recommended way to refer to this notation in names is `not`.
 -/
 @[inline] def Bool.not : Bool → Bool
   | true  => false