feat: suggestions for some size/count/length confusions

doc/std/naming.md

@@ -257,4 +257,13 @@ We make the following recommendations for variable names, but without insisting
 * `i`, `j`, `k` are preferred for numerical indices.
   Descriptive names such as `start`, `stop`, `lo`, and `hi` are encouraged when they increase readability.
 * `n`, `m` are preferred for sizes, e.g. in `Vector α n` or `xs.size = n`.
-* `w` is preferred for the width of a `BitVec`.
+* `w` is preferred for the width of a `BitVec`.
+
+## Suggestions
+
+When names are difficult to guess due to inconsistency between standard libraries from different languages (e.g. `List.all` in most programming languages is `List.every` in JavaScript) or are subtle within Lean's standard library (`Array.size` and `Slice.size` subtly indicate a constant-time operation, whereas `List.length` and `String.length` are linear-time operations), the `suggest_for` option can be used to clue users who guess the wrong name.
+
+```lean
+@[suggest_for String.size]
+def String.length (b : @& String) : Nat := ...
+```

src/Init/Data/Array/Subarray.lean

@@ -80,6 +80,7 @@ namespace Subarray
 /--
 Computes the size of the subarray.
 -/
+@[suggest_for Subarray.length]
 def size (s : Subarray α) : Nat :=
   s.stop - s.start
 

src/Init/Data/FloatArray/Basic.lean

@@ -42,7 +42,7 @@ instance : EmptyCollection FloatArray where
 def push : FloatArray → Float → FloatArray
   | ⟨ds⟩, b => ⟨ds.push b⟩
 
-@[extern "lean_float_array_size", tagged_return]
+@[extern "lean_float_array_size", tagged_return, suggest_for FloatArray.length]
 def size : (@& FloatArray) → Nat
   | ⟨ds⟩ => ds.size
 

src/Init/Data/Iterators/Consumers/Loop.lean

@@ -637,7 +637,7 @@ Steps through the whole iterator, counting the number of outputs emitted.
 
 This function's runtime is linear in the number of steps taken by the iterator.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline, expose, suggest_for Std.Iterators.Iter.length Std.Iterators.Iter.Partial.length]
 def Iter.count {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
     (it : Iter (α := α) β) : Nat :=
   it.toIterM.count.run.down

src/Init/Data/Iterators/Consumers/Monadic/Loop.lean

@@ -901,7 +901,7 @@ Steps through the whole iterator, counting the number of outputs emitted.
 
 This function's runtime is linear in the number of steps taken by the iterator.
 -/
-@[always_inline, inline]
+@[always_inline, inline, suggest_for Std.Iterators.IterM.length Std.Iterators.IterM.Partial.length]
 def IterM.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     [IteratorLoop α m m] [Monad m] (it : IterM (α := α) m β) : m (ULift Nat) :=
   it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)

src/Init/Data/RArray.lean

@@ -65,6 +65,7 @@ theorem RArray.get_eq_getImpl : @RArray.get = @RArray.getImpl := by
 instance : GetElem (RArray α) Nat α (fun _ _ => True) where
   getElem a n _ := a.get n
 
+@[suggest_for Lean.RArray.length]
 def RArray.size : RArray α → Nat
   | leaf _ => 1
   | branch _ l r => l.size + r.size

src/Init/Data/Range/Basic.lean

@@ -26,7 +26,8 @@ namespace Range
 universe u v
 
 /-- The number of elements in the range. -/
-@[simp, expose] def size (r : Range) : Nat := (r.stop - r.start + r.step - 1) / r.step
+@[simp, expose, suggest_for Std.Range.length]
+def size (r : Range) : Nat := (r.stop - r.start + r.step - 1) / r.step
 
 @[inline] protected def forIn' [Monad m] (range : Range) (init : β)
     (f : (i : Nat) → i ∈ range → β → m (ForInStep β)) : m β :=

src/Init/Data/Slice/Operations.lean

@@ -52,7 +52,7 @@ Returns the number of elements with distinct indices in the given slice.
 
 Example: `#[1, 1, 1][0...2].size = 2`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, suggest_for Std.Slice.length]
 def size (s : Slice γ) [SliceSize γ] :=
   SliceSize.size s
 

src/Init/Data/String/Basic.lean

@@ -264,7 +264,7 @@ Examples:
 * `"abc".length = 3`
 * `"L∃∀N".length = 4`
 -/
-@[extern "lean_string_length", expose, tagged_return]
+@[extern "lean_string_length", expose, tagged_return, suggest_for String.size]
 def String.length (b : @& String) : Nat :=
   b.toList.length
 

src/Init/Data/String/Bootstrap.lean

@@ -64,7 +64,7 @@ opaque offsetOfPos (s : String) (pos : Pos.Raw) : Nat
 @[extern "lean_string_utf8_extract"]
 opaque extract : (@& String) → (@& Pos.Raw) → (@& Pos.Raw) → String
 
-@[extern "lean_string_length"]
+@[extern "lean_string_length", suggest_for String.Internal.size]
 opaque length : (@& String) → Nat
 
 @[extern "lean_string_pushn"]

src/Init/Data/Vector/Basic.lean

@@ -42,6 +42,7 @@ abbrev Array.toVector (xs : Array α) : Vector α xs.size := .mk xs rfl
 namespace Vector
 
 /-- The size of a vector. -/
+@[suggest_for Vector.length]
 abbrev size {α n} (_ : Vector α n) : Nat := n
 
 /-- Syntax for `Vector α n` -/

src/Init/Prelude.lean

@@ -2992,7 +2992,7 @@ Examples:
  * `([] : List String).length = 0`
  * `["green", "brown"].length = 2`
 -/
-def List.length : List α → Nat
+@[suggest_for List.size] def List.length : List α → Nat
   | nil       => 0
   | cons _ as => HAdd.hAdd (length as) 1
 
@@ -3202,7 +3202,7 @@ This is a cached value, so it is `O(1)` to access. The space allocated for an ar
 its _capacity_, is at least as large as its size, but may be larger. The capacity of an array is an
 internal detail that's not observable by Lean code.
 -/
-@[extern "lean_array_get_size", tagged_return]
+@[extern "lean_array_get_size", tagged_return, suggest_for Array.length]
 def Array.size {α : Type u} (a : @& Array α) : Nat :=
  a.toList.length
 
@@ -3410,7 +3410,7 @@ Returns the number of bytes in the byte array.
 This is the number of bytes actually in the array, as distinct from its capacity, which is the
 amount of memory presently allocated for the array.
 -/
-@[extern "lean_byte_array_size", tagged_return]
+@[extern "lean_byte_array_size", tagged_return, suggest_for ByteArray.length]
 def ByteArray.size : (@& ByteArray) → Nat
   | ⟨bs⟩ => bs.size
 

src/Lean/Data/KVMap.lean

@@ -80,6 +80,7 @@ def empty : KVMap :=
 def isEmpty : KVMap → Bool
   | ⟨m⟩ => m.isEmpty
 
+@[suggest_for Lean.KVMap.length]
 def size (m : KVMap) : Nat :=
   m.entries.length