feat: suggestions for some size/count/length confusions

Author: robsimmons

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

@@ -636,7 +636,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

@@ -900,7 +900,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"]