diff --git a/doc/std/naming.md b/doc/std/naming.md index 032400c93893..d20e75cc5746 100644 --- a/doc/std/naming.md +++ b/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`. \ No newline at end of file +* `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 := ... +``` \ No newline at end of file diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean index 50772392ba27..ef516b23fcba 100644 --- a/src/Init/Data/Array/Subarray.lean +++ b/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 diff --git a/src/Init/Data/FloatArray/Basic.lean b/src/Init/Data/FloatArray/Basic.lean index 3ed6826742b0..d79a1538e788 100644 --- a/src/Init/Data/FloatArray/Basic.lean +++ b/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 diff --git a/src/Init/Data/Iterators/Consumers/Loop.lean b/src/Init/Data/Iterators/Consumers/Loop.lean index 3531e4050772..bef273f7b0c7 100644 --- a/src/Init/Data/Iterators/Consumers/Loop.lean +++ b/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 diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean index 31aabe1bc3bc..3dc2646d7d25 100644 --- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean +++ b/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) diff --git a/src/Init/Data/RArray.lean b/src/Init/Data/RArray.lean index 74d39622a927..2943a2b860d9 100644 --- a/src/Init/Data/RArray.lean +++ b/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 diff --git a/src/Init/Data/Range/Basic.lean b/src/Init/Data/Range/Basic.lean index 4c9c3e96eef6..241aa3469cd7 100644 --- a/src/Init/Data/Range/Basic.lean +++ b/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 β := diff --git a/src/Init/Data/Slice/Operations.lean b/src/Init/Data/Slice/Operations.lean index ffdb849ae6cf..a5e927509c5b 100644 --- a/src/Init/Data/Slice/Operations.lean +++ b/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 diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 42f4b1b23603..ef9e549e14a8 100644 --- a/src/Init/Data/String/Basic.lean +++ b/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 diff --git a/src/Init/Data/String/Bootstrap.lean b/src/Init/Data/String/Bootstrap.lean index f7ab509a5de6..087ab5bfb262 100644 --- a/src/Init/Data/String/Bootstrap.lean +++ b/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"] diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean index 8755e112fc89..1eb18988bbf2 100644 --- a/src/Init/Data/Vector/Basic.lean +++ b/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` -/ diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 807f073e1430..091874ba2529 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -2975,7 +2975,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 @@ -3185,7 +3185,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 @@ -3393,7 +3393,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 diff --git a/src/Lean/Data/KVMap.lean b/src/Lean/Data/KVMap.lean index 9030058ef935..da83c5bd8144 100644 --- a/src/Lean/Data/KVMap.lean +++ b/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