doc: review of Array docstrings for manual (#7492)

This PR adds missing `Array` docstrings and makes their style
consistent.

src/Init/Data/Array/Attach.lean

@@ -15,13 +15,12 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
 namespace Array
 
 /--
-`O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on
-`a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l`
-but is defined only when all members of `l` satisfy `P`, using the proof
-to apply `f`.
+Maps a partially defined function (defined on those terms of `α` that satisfy a predicate `P`) over
+an array `xs : Array α`, given a proof that every element of `xs` in fact satisfies `P`.
 
-We replace this at runtime with a more efficient version via the `csimp` lemma `pmap_eq_pmapImpl`.
+`Array.pmap`, named for “partial map,” is the equivalent of `Array.map` for such partial functions.
 -/
+
 def pmap {P : α → Prop} (f : ∀ a, P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a) : Array β :=
   (xs.toList.pmap f (fun a m => H a (mem_def.mpr m))).toArray
 
@@ -32,14 +31,27 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
 @[inline] private unsafe def attachWithImpl
     (xs : Array α) (P : α → Prop) (_ : ∀ x ∈ xs, P x) : Array {x // P x} := unsafeCast xs
 
-/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `xs` to produce a new array
-  with the same elements but in the type `{x // P x}`. -/
+/--
+“Attaches” individual proofs to an array of values that satisfy a predicate `P`, returning an array
+of elements in the corresponding subtype `{ x // P x }`.
+
+`O(1)`.
+-/
 @[implemented_by attachWithImpl] def attachWith
     (xs : Array α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Array {x // P x} :=
   ⟨xs.toList.attachWith P fun x h => H x (Array.Mem.mk h)⟩
 
-/-- `O(1)`. "Attach" the proof that the elements of `xs` are in `xs` to produce a new array
-  with the same elements but in the type `{x // x ∈ xs}`. -/
+/--
+“Attaches” the proof that the elements of `xs` are in fact elements of `xs`, producing a new array with
+the same elements but in the subtype `{ x // x ∈ xs }`.
+
+`O(1)`.
+
+This function is primarily used to allow definitions by [well-founded
+recursion](lean-manual://section/well-founded-recursion) that use higher-order functions (such as
+`Array.map`) to prove that an value taken from a list is smaller than the list. This allows the
+well-founded recursion mechanism to prove that the function terminates.
+-/
 @[inline] def attach (xs : Array α) : Array {x // x ∈ xs} := xs.attachWith _ fun _ => id
 
 @[simp] theorem _root_.List.attachWith_toArray {l : List α} {P : α → Prop} {H : ∀ x ∈ l.toArray, P x} :
@@ -542,11 +554,19 @@ Further, we provide simp lemmas that push `unattach` inwards.
 -/
 
 /--
-A synonym for `l.map (·.val)`. Mostly this should not be needed by users.
-It is introduced as in intermediate step by lemmas such as `map_subtype`,
-and is ideally subsequently simplified away by `unattach_attach`.
+Maps an array of terms in a subtype to the corresponding terms in the type by forgetting that they
+satisfy the predicate.
 
-If not, usually the right approach is `simp [Array.unattach, -Array.map_subtype]` to unfold.
+This is the inverse of `Array.attachWith` and a synonym for `xs.map (·.val)`.
+
+Mostly this should not be needed by users. It is introduced as an intermediate step by lemmas such
+as `map_subtype`, and is ideally subsequently simplified away by `unattach_attach`.
+
+This function is usually inserted automatically by Lean as an intermediate step while proving
+termination. It is rarely used explicitly in code. It is introduced as an intermediate step during
+the elaboration of definitions by [well-founded
+recursion](lean-manual://section/well-founded-recursion). If this function is encountered in a proof
+state, the right approach is usually the tactic `simp [Array.unattach, -Array.map_subtype]`.
 -/
 def unattach {α : Type _} {p : α → Prop} (xs : Array { x // p x }) : Array α := xs.map (·.val)
 

src/Init/Data/Array/BasicAux.lean

@@ -38,6 +38,11 @@ private theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Arra
 theorem List.toArray_eq_toArray_eq (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by
   simp
 
+/--
+Applies the monadic action `f` to every element in the array, left-to-right, and returns the array
+of results. Furthermore, the resulting array's type guarantees that it contains the same number of
+elements as the input array.
+-/
 def Array.mapM' [Monad m] (f : α → m β) (as : Array α) : m { bs : Array β // bs.size = as.size } :=
   go 0 ⟨mkEmpty as.size, rfl⟩ (by simp)
 where
@@ -66,11 +71,19 @@ where
       return as
 
 /--
-Monomorphic `Array.mapM`. The internal implementation uses pointer equality, and does not allocate a new array
-if the result of each `f a` is a pointer equal value `a`.
+Applies a monadic function to each element of an array, returning the array of results. The function is
+monomorphic: it is required to return a value of the same type. The internal implementation uses
+pointer equality, and does not allocate a new array if the result of each function call is
+pointer-equal to its argument.
 -/
 @[implemented_by mapMonoMImp] def Array.mapMonoM [Monad m] (as : Array α) (f : α → m α) : m (Array α) :=
   as.mapM f
 
+/--
+Applies a function to each element of an array, returning the array of results. The function is
+monomorphic: it is required to return a value of the same type. The internal implementation uses
+pointer equality, and does not allocate a new array if the result of each function call is
+pointer-equal to its argument.
+-/
 @[inline] def Array.mapMono (as : Array α) (f : α → α) : Array α :=
   Id.run <| as.mapMonoM f

src/Init/Data/Array/BinSearch.lean

@@ -29,6 +29,16 @@ namespace Array
     else found (some a)
 termination_by lo hi => hi.1 - lo.1
 
+/--
+Binary search for an element equivalent to `k` in the sorted array `as`. Returns the element from
+the array, if it is found, or `none` otherwise.
+
+The array `as` must be sorted according to the comparison operator `lt`, which should be a total
+order.
+
+The optional parameters `lo` and `hi` determine the region of the array indices to be searched. Both
+are inclusive, and default to searching the entire array.
+-/
 @[inline] def binSearch {α : Type} (as : Array α) (k : α) (lt : α → α → Bool) (lo := 0) (hi := as.size - 1) : Option α :=
   if h : lo < as.size then
     let hi := if hi < as.size then hi else as.size - 1
@@ -39,6 +49,16 @@ termination_by lo hi => hi.1 - lo.1
   else
     none
 
+/--
+Binary search for an element equivalent to `k` in the sorted array `as`. Returns `true` if the
+element is found, or `false` otherwise.
+
+The array `as` must be sorted according to the comparison operator `lt`, which should be a total
+order.
+
+The optional parameters `lo` and `hi` determine the region of the array indices to be searched. Both
+are inclusive, and default to searching the entire array.
+-/
 @[inline] def binSearchContains {α : Type} (as : Array α) (k : α) (lt : α → α → Bool) (lo := 0) (hi := as.size - 1) : Bool :=
   if h : lo < as.size then
     let hi := if hi < as.size then hi else as.size - 1
@@ -68,6 +88,16 @@ termination_by lo hi => hi.1 - lo.1
       as.modifyM mid <| fun v => merge v
 termination_by lo hi => hi.1 - lo.1
 
+/--
+Inserts an element `k` into a sorted array `as` such that the resulting array is sorted.
+
+The ordering predicate `lt` should be a total order on elements, and the array `as` should be sorted
+with respect to `lt`.
+
+If an element that `lt` equates to `k` is already present in `as`, then `merge` is applied to the
+existing element to determine the value of that position in the resulting array. If no element equal
+to `k` is present, then `add` is used to determine the value to be inserted.
+-/
 @[specialize] def binInsertM {α : Type u} {m : Type u → Type v} [Monad m]
     (lt : α → α → Bool)
     (merge : α → m α)
@@ -81,6 +111,21 @@ termination_by lo hi => hi.1 - lo.1
   else if !lt k as[as.size - 1] then as.modifyM (as.size - 1) <| merge
   else binInsertAux lt merge add as k ⟨0, by omega⟩ ⟨as.size - 1, by omega⟩ (by simp) (by simpa using h')
 
+/--
+Inserts an element into a sorted array such that the resulting array is sorted. If the element is
+already present in the array, it is not inserted.
+
+The ordering predicate `lt` should be a total order on elements, and the array `as` should be sorted
+with respect to `lt`.
+
+`Array.binInsertM` is a more general operator that provides greater control over the handling of
+duplicate elements in addition to running in a monad.
+
+Examples:
+* `#[0, 1, 3, 5].binInsert (· < ·) 2 = #[0, 1, 2, 3, 5]`
+* `#[0, 1, 3, 5].binInsert (· < ·) 1 = #[0, 1, 3, 5]`
+* `#[].binInsert (· < ·) 1 = #[1]`
+-/
 @[inline] def binInsert {α : Type u} (lt : α → α → Bool) (as : Array α) (k : α) : Array α :=
   Id.run <| binInsertM lt (fun _ => k) (fun _ => k) as k
 

src/Init/Data/Array/FinRange.lean

@@ -12,7 +12,13 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
 
 namespace Array
 
-/-- `finRange n` is the array of all elements of `Fin n` in order. -/
+/--
+Returns an array of all elements of `Fin n` in order, starting at `0`.
+
+Examples:
+ * `Array.finRange 0 = (#[] : Array (Fin 0))`
+ * `Array.finRange 2 = (#[0, 1] : Array (Fin 2))`
+-/
 protected def finRange (n : Nat) : Array (Fin n) := ofFn fun i => i
 
 @[simp] theorem size_finRange (n) : (Array.finRange n).size = n := by

src/Init/Data/Array/InsertionSort.lean

@@ -9,6 +9,12 @@ import Init.Data.Array.Basic
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
+/--
+Sorts an array using insertion sort.
+
+The optional parameter `lt` specifies an ordering predicate. It defaults to `LT.lt`, which must be
+decidable to be used for sorting.
+-/
 @[inline] def Array.insertionSort (xs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Array α :=
   traverse xs 0 xs.size
 where

src/Init/Data/Array/Lemmas.lean

@@ -3921,7 +3921,15 @@ theorem all_reverse {xs : Array α} : xs.reverse.all f 0 = xs.all f := by
 
 /-! ### toListRev -/
 
-/-- A more efficient version of `arr.toList.reverse`; for verification purposes we immediately simplify it. -/
+/--
+Converts an array to a list that contains the same elements in the opposite order.
+
+This is equivalent to, but more efficient than, `Array.toList ∘ List.reverse`.
+
+Examples:
+* `#[1, 2, 3].toListRev = [3, 2, 1]`
+* `#["blue", "yellow"].toListRev = ["yellow", "blue"]`
+-/
 @[inline] def toListRev (xs : Array α) : List α := xs.foldl (fun l t => t :: l) []
 
 @[simp] theorem toListRev_eq (xs : Array α) : xs.toListRev = xs.toList.reverse := by

src/Init/Data/Array/Lex/Basic.lean

@@ -14,11 +14,12 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
 namespace Array
 
 /--
-Lexicographic comparator for arrays.
+Compares arrays lexicographically with respect to a comparison `lt` on their elements.
 
-`lex as bs lt` is true if
-- `bs` is larger than `as` and `as` is pairwise equivalent via `==` to the initial segment of `bs`, or
-- there is an index `i` such that `lt as[i] bs[i]`, and for all `j < i`, `as[j] == bs[j]`.
+Specifically, `Array.lex as bs lt` is true if
+* `bs` is larger than `as` and `as` is pairwise equivalent via `==` to the initial segment of `bs`,
+  or
+* there is an index `i` such that `lt as[i] bs[i]`, and for all `j < i`, `as[j] == bs[j]`.
 -/
 def lex [BEq α] (as bs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Bool := Id.run do
   for h : i in [0 : min as.size bs.size] do

src/Init/Data/Array/QSort.lean

@@ -30,6 +30,16 @@ private def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi :
       (⟨i, ilo⟩, as.swap i hi)
   loop as lo lo
 
+/--
+Sorts an array using the Quicksort algorithm.
+
+The optional parameter `lt` specifies an ordering predicate. It defaults to `LT.lt`, which must be
+decidable to be used for sorting. Use `Array.qsortOrd` to sort the array according to the `Ord α`
+instance.
+
+The optional parameters `low` and `high` delimit the region of the array that is sorted. Both are
+inclusive, and default to sorting the entire array.
+-/
 @[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·))
     (low := 0) (high := as.size - 1) : Array α :=
   let rec @[specialize] sort {n} (as : Vector α n) (lo hi : Nat)
@@ -50,7 +60,7 @@ private def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi :
 
 set_option linter.unusedVariables.funArgs false in
 /--
-Sort an array using `compare` to compare elements.
+Sorts an array using the Quicksort algorithm, using `Ord.compare` to compare elements.
 -/
 def qsortOrd [ord : Ord α] (xs : Array α) : Array α :=
   xs.qsort fun x y => compare x y |>.isLT

src/Init/Data/Array/Set.lean

@@ -11,11 +11,16 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
 
 
 /--
-Set an element in an array, using a proof that the index is in bounds.
-(This proof can usually be omitted, and will be synthesized automatically.)
+Replaces the element at a given index in an array.
 
-This will perform the update destructively provided that `a` has a reference
-count of 1 when called.
+No bounds check is performed, but the function requires a proof that the index is in bounds. This
+proof can usually be omitted, and will be synthesized automatically.
+
+The array is modified in-place if there are no other references to it.
+
+Examples:
+* `#[0, 1, 2].set 1 5 = #[0, 5, 2]`
+* `#["orange", "apple"].set 1 "grape" = #["orange", "grape"]`
 -/
 @[extern "lean_array_fset"]
 def Array.set (xs : Array α) (i : @& Nat) (v : α) (h : i < xs.size := by get_elem_tactic) :
@@ -23,10 +28,15 @@ def Array.set (xs : Array α) (i : @& Nat) (v : α) (h : i < xs.size := by get_e
   toList := xs.toList.set i v
 
 /--
-Set an element in an array, or do nothing if the index is out of bounds.
+Replaces the element at the provided index in an array. The array is returned unmodified if the
+index is out of bounds.
 
-This will perform the update destructively provided that `a` has a reference
-count of 1 when called.
+The array is modified in-place if there are no other references to it.
+
+Examples:
+* `#[0, 1, 2].setIfInBounds 1 5 = #[0, 5, 2]`
+* `#["orange", "apple"].setIfInBounds 1 "grape" = #["orange", "grape"]`
+* `#["orange", "apple"].setIfInBounds 5 "grape" = #["orange", "apple"]`
 -/
 @[inline] def Array.setIfInBounds (xs : Array α) (i : Nat) (v : α) : Array α :=
   dite (LT.lt i xs.size) (fun h => xs.set i v h) (fun _ => xs)

src/Init/Data/List/Attach.lean

@@ -41,7 +41,7 @@ elements in the corresponding subtype `{ x // P x }`.
     (l : List α) (P : α → Prop) (H : ∀ x ∈ l, P x) : List {x // P x} := pmap Subtype.mk l H
 
 /--
-"Attaches" the proof that the elements of `l` are in fact elements of `l`, producing a new list with
+“Attaches” the proof that the elements of `l` are in fact elements of `l`, producing a new list with
 the same elements but in the subtype `{ x // x ∈ l }`.
 
 `O(1)`.

src/Init/Data/List/Basic.lean

@@ -259,7 +259,7 @@ instance decidableLE [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List
   inferInstanceAs (Decidable (Not _))
 
 /--
-Compare lists lexicographically with respect to a comparison on their elements.
+Compares lists lexicographically with respect to a comparison on their elements.
 
 The lexicographic order with respect to `lt` is:
 * `[].lex (b :: bs)` is `true`
@@ -493,7 +493,7 @@ Returns the list of elements in `l` for which `p` returns `true`.
 `O(|l|)`.
 
 Examples:
-* `[1, 2, 5, 2, 7, 7].filter (· > 2)  = [5, 7, 7]`
+* `[1, 2, 5, 2, 7, 7].filter (· > 2) = [5, 7, 7]`
 * `[1, 2, 5, 2, 7, 7].filter (fun _ => false) = []`
 * `[1, 2, 5, 2, 7, 7].filter (fun _ => true) = [1, 2, 5, 2, 7, 7]`
 -/
@@ -766,10 +766,10 @@ Pads `l : List α` on the left with repeated occurrences of `a : α` until it is
 already has at least `n` elements, it is returned unmodified.
 
 Examples:
- * `[1, 2, 3].leftPad 5 0 = [0, 0, 1, 2, 3]`
- * `["red", "green", "blue"].leftPad 4 "blank" = ["blank", "red", "green", "blue"]`
- * `["red", "green", "blue"].leftPad 3 "blank" = ["red", "green", "blue"]`
- * `["red", "green", "blue"].leftPad 1 "blank" = ["red", "green", "blue"]`
+ * `[1, 2, 3].leftpad 5 0 = [0, 0, 1, 2, 3]`
+ * `["red", "green", "blue"].leftpad 4 "blank" = ["blank", "red", "green", "blue"]`
+ * `["red", "green", "blue"].leftpad 3 "blank" = ["red", "green", "blue"]`
+ * `["red", "green", "blue"].leftpad 1 "blank" = ["red", "green", "blue"]`
 -/
 def leftpad (n : Nat) (a : α) (l : List α) : List α := replicate (n - length l) a ++ l
 
@@ -779,10 +779,10 @@ Pads `l : List α` on the right with repeated occurrences of `a : α` until it i
 `l` already has at least `n` elements, it is returned unmodified.
 
 Examples:
- * `[1, 2, 3].rightPad 5 0 = [1, 2, 3, 0, 0]`
- * `["red", "green", "blue"].rightPad 4 "blank" = ["red", "green", "blue", "blank"]`
- * `["red", "green", "blue"].rightPad 3 "blank" = ["red", "green", "blue"]`
- * `["red", "green", "blue"].rightPad 1 "blank" = ["red", "green", "blue"]`
+ * `[1, 2, 3].rightpad 5 0 = [1, 2, 3, 0, 0]`
+ * `["red", "green", "blue"].rightpad 4 "blank" = ["red", "green", "blue", "blank"]`
+ * `["red", "green", "blue"].rightpad 3 "blank" = ["red", "green", "blue"]`
+ * `["red", "green", "blue"].rightpad 1 "blank" = ["red", "green", "blue"]`
 -/
 def rightpad (n : Nat) (a : α) (l : List α) : List α := l ++ replicate (n - length l) a
 
@@ -1702,7 +1702,6 @@ Examples:
 * `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = some 4`
 * `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = none`
 -/
-
 def findIdx? (p : α → Bool) (l : List α) : Option Nat :=
   go l 0
 where
@@ -1866,7 +1865,7 @@ def isPerm [BEq α] : List α → List α → Bool
 /-! ### any -/
 
 /--
-Returns true if `p` returns `true` for any element of `l`.
+Returns `true` if `p` returns `true` for any element of `l`.
 
 `O(|l|)`. Short-circuits upon encountering the first `true`.
 
@@ -1886,7 +1885,7 @@ def any : (l : List α) → (p : α → Bool) → Bool
 /-! ### all -/
 
 /--
-Returns true if `p` returns `true` for every element of `l`.
+Returns `true` if `p` returns `true` for every element of `l`.
 
 `O(|l|)`. Short-circuits upon encountering the first `false`.
 
@@ -1966,7 +1965,7 @@ Examples:
 
 /--
 Combines two lists into a list of pairs in which the first and second components are the
-corresponding elements of each list. The resulting list is the length of the shorter of the inputs
+corresponding elements of each list. The resulting list is the length of the shorter of the input
 lists.
 
 `O(min |xs| |ys|)`.

src/Init/Data/List/Control.lean

@@ -46,7 +46,7 @@ Users that want to use `mapM` with `Applicative` should use `mapA` instead.
 -/
 
 /--
-Applies the monadic action `f` on every element in the list, left-to-right, and returns the list of
+Applies the monadic action `f` to every element in the list, left-to-right, and returns the list of
 results.
 
 This implementation is tail recursive. `List.mapM'` is a a non-tail-recursive variant that may be
@@ -243,7 +243,7 @@ def foldlM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (f : s
 
 /--
 Folds a monadic function over a list from the right, accumulating a value starting with `init`. The
-accumulated value is combined with the each element of the list in order, using `f`.
+accumulated value is combined with the each element of the list in reverse order, using `f`.
 
 Example:
 ```lean example

src/Init/Data/List/FinRange.lean

@@ -15,8 +15,8 @@ namespace List
 Lists all elements of `Fin n` in order, starting at `0`.
 
 Examples:
- * `List.finRange 0 = ([] : List Fin 0)`
- * `List.finRange 2 = ([0, 1] : List Fin 2)`
+ * `List.finRange 0 = ([] : List (Fin 0))`
+ * `List.finRange 2 = ([0, 1] : List (Fin 2))`
 -/
 def finRange (n : Nat) : List (Fin n) := ofFn fun i => i
 

src/Init/Data/Vector/Basic.lean

@@ -29,7 +29,9 @@ deriving Repr, DecidableEq
 
 attribute [simp] Vector.size_toArray
 
-/-- Convert `xs : Array α` to `Vector α xs.size`. -/
+/--
+Converts an array to a vector. The resulting vector's size is the array's size.
+-/
 abbrev Array.toVector (xs : Array α) : Vector α xs.size := .mk xs rfl
 
 namespace Vector

src/Init/Meta.lean

@@ -1207,9 +1207,19 @@ private partial def filterSepElemsMAux {m : Type → Type} [Monad m] (a : Array
   else
     pure acc
 
+/--
+Filters an array of syntax, treating every other element as a separator rather than an element to
+test with the monadic predicate `p`. The resulting array contains the tested elements for which `p`
+returns `true`, separated by the corresponding separator elements.
+-/
 def filterSepElemsM {m : Type → Type} [Monad m] (a : Array Syntax) (p : Syntax → m Bool) : m (Array Syntax) :=
   filterSepElemsMAux a p 0 #[]
 
+/--
+Filters an array of syntax, treating every other element as a separator rather than an element to
+test with the predicate `p`. The resulting array contains the tested elements for which `p` returns
+`true`, separated by the corresponding separator elements.
+-/
 def filterSepElems (a : Array Syntax) (p : Syntax → Bool) : Array Syntax :=
   Id.run <| a.filterSepElemsM p
 

src/Init/Prelude.lean

@@ -2717,45 +2717,47 @@ def panic {α : Sort u} [Inhabited α] (msg : String) : α :=
 attribute [nospecialize] Inhabited
 
 /--
-`Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)
-with elements from `α`. This type has special support in the runtime.
+`Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array) with elements
+from `α`. This type has special support in the runtime.
 
-Arrays perform best when unshared; as long
-as they are used "linearly" all updates will be performed destructively on the
-array, so it has comparable performance to mutable arrays in imperative
-programming languages.
+Arrays perform best when unshared. As long as there is never more than one reference to an array,
+all updates will be performed _destructively_. This results in performance comparable to mutable
+arrays in imperative programming languages.
 
-An array has a size and a capacity; the size is `Array.size` but the capacity
-is not observable from Lean code. `Array.emptyWithCapacity n` creates an array which is equal to `#[]`,
-but internally allocates an array of capacity `n`.
+An array has a size and a capacity. The size is the number of elements present in the array, while
+the capacity is the amount of memory currently allocated for elements. The size is accessible via
+`Array.size`, but the capacity is not observable from Lean code. `Array.emptyWithCapacity n` creates
+an array which is equal to `#[]`, but internally allocates an array of capacity `n`. When the size
+exceeds the capacity, allocation is required to grow the array.
 
-From the point of view of proofs `Array α` is just a wrapper around `List α`.
+From the point of view of proofs, `Array α` is just a wrapper around `List α`.
 -/
 structure Array (α : Type u) where
   /--
   Converts a `List α` into an `Array α`.
 
-  You can also use the synonym `List.toArray` when dot notation is convenient.
+  The function `List.toArray` is preferred.
 
-  At runtime, this constructor is implemented by `List.toArrayImpl` and is O(n) in the length of the
-  list.
+  At runtime, this constructor is overridden by `List.toArrayImpl` and is `O(n)` in the length of
+  the list.
   -/
   mk ::
   /--
-  Converts a `Array α` into an `List α`.
+  Converts an `Array α` into a `List α` that contains the same elements in the same order.
 
-  At runtime, this projection is implemented by `Array.toListImpl` and is O(n) in the length of the
-  array. -/
+  At runtime, this is implemented by `Array.toListImpl` and is `O(n)` in the length of the
+  array.
+  -/
   toList : List α
 
 attribute [extern "lean_array_to_list"] Array.toList
 attribute [extern "lean_array_mk"] Array.mk
 
 /--
-Converts a `List α` into an `Array α`. `O(|xs|)`.
+Converts a `List α` into an `Array α`.
 
-At runtime, this operation is implemented by `List.toArrayImpl` and takes time linear in the length
-of the list. `List.toArray` should be used instead of `Array.mk`.
+ `O(|xs|)`. At runtime, this operation is implemented by `List.toArrayImpl` and takes time linear in
+the length of the list. `List.toArray` should be used instead of `Array.mk`.
 
 Examples:
  * `[1, 2, 3].toArray = #[1, 2, 3]`
@@ -2764,7 +2766,8 @@ Examples:
 @[match_pattern]
 abbrev List.toArray (xs : List α) : Array α := .mk xs
 
-/-- Construct a new empty array with initial capacity `c`.
+/--
+Constructs a new empty array with initial capacity `c`.
 
 This will be deprecated in favor of `Array.emptyWithCapacity` in the future.
 -/
@@ -2774,14 +2777,26 @@ def Array.mkEmpty {α : Type u} (c : @& Nat) : Array α where
 
 
 set_option linter.unusedVariables false in
-/-- Construct a new empty array with initial capacity `c`. -/
+/--
+Constructs a new empty array with initial capacity `c`.
+-/
 def Array.emptyWithCapacity {α : Type u} (c : @& Nat) : Array α where
   toList := List.nil
 
-/-- Construct a new empty array. -/
+/--
+Constructs a new empty array with initial capacity `0`.
+
+Use `Array.emptyWithCapacity` to create an array with a greater initial capacity.
+-/
 def Array.empty {α : Type u} : Array α := emptyWithCapacity 0
 
-/-- Get the size of an array. This is a cached value, so it is O(1) to access. -/
+/--
+Gets the number of elements stored in an array.
+
+This is a cached value, so it is `O(1)` to access. The space allocated for an array, referred to as
+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.
+-/
 @[reducible, extern "lean_array_get_size"]
 def Array.size {α : Type u} (a : @& Array α) : Nat :=
  a.toList.length
@@ -2800,7 +2815,18 @@ arrays.
 def Array.getInternal {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α :=
   a.toList.get ⟨i, h⟩
 
-/-- Access an element from an array, or return `v₀` if the index is out of bounds. -/
+/--
+Returns the element at the provided index, counting from `0`. Returns the fallback value `v₀` if the
+index is out of bounds.
+
+To return an `Option` depending on whether the index is in bounds, use `a[i]?`. To panic if the
+index is out of bounds, use `a[i]!`.
+
+Examples:
+ * `#["spring", "summer", "fall", "winter"].getD 2 "never" = "fall"`
+ * `#["spring", "summer", "fall", "winter"].getD 0 "never" = "spring"`
+ * `#["spring", "summer", "fall", "winter"].getD 4 "never" = "never"`
+-/
 @[inline] abbrev Array.getD (a : Array α) (i : Nat) (v₀ : α) : α :=
   dite (LT.lt i a.size) (fun h => a.getInternal i h) (fun _ => v₀)
 
@@ -2814,8 +2840,14 @@ def Array.get!Internal {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Na
   Array.getD a i default
 
 /--
-Push an element onto the end of an array. This is amortized O(1) because
-`Array α` is internally a dynamic array.
+Adds an element to the end of an array. The resulting array's size is one greater than the input
+array. If there are no other references to the array, then it is modified in-place.
+
+This takes amortized `O(1)` time because `Array α` is represented by a dynamic array.
+
+Examples:
+* `#[].push "apple" = #["apple"]`
+* `#["apple"].push "orange" = #["apple", "orange"]`
 -/
 @[extern "lean_array_push"]
 def Array.push {α : Type u} (a : Array α) (v : α) : Array α where
@@ -2869,9 +2901,21 @@ protected def Array.appendCore {α : Type u}  (as : Array α) (bs : Array α) :
   loop bs.size 0 as
 
 /--
-  Returns the slice of `as` from indices `start` to `stop` (exclusive).
-  If `start` is greater or equal to `stop`, the result is empty.
-  If `stop` is greater than the length of `as`, the length is used instead. -/
+Returns the slice of `as` from indices `start` to `stop` (exclusive). The resulting array has size
+`(min stop as.size) - start`.
+
+If `start` is greater or equal to `stop`, the result is empty. If `stop` is greater than the size of
+`as`, the size is used instead.
+
+Examples:
+ * `#[0, 1, 2, 3, 4].extract 1 3 = #[1, 2]`
+ * `#[0, 1, 2, 3, 4].extract 1 30 = #[1, 2, 3, 4]`
+ * `#[0, 1, 2, 3, 4].extract 0 0 = #[]`
+ * `#[0, 1, 2, 3, 4].extract 2 1 = #[]`
+ * `#[0, 1, 2, 3, 4].extract 2 2 = #[]`
+ * `#[0, 1, 2, 3, 4].extract 2 3 = #[2]`
+ * `#[0, 1, 2, 3, 4].extract 2 4 = #[2, 3]`
+-/
 -- NOTE: used in the quotation elaborator output
 def Array.extract (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : Array α :=
   let rec loop (i : Nat) (j : Nat) (bs : Array α) : Array α :=

src/Lean/Data/Array.lean

@@ -15,12 +15,22 @@ is part of the public, user-facing standard library.
 -/
 
 /--
-Given an array `a`, runs `f xᵢ xⱼ` for all `i < j`, removes those entries for which `f` returns
-`false` (and will subsequently skip pairs if one element is removed), and returns the array of
-remaining elements.
+Compares each element of an array with all later elements using `f`. For each comparison, `f`
+determines whether to keep both of its arguments. If `f` returns `false` for an argument, that
+argument is removed from the array and does not participate in subsequent comparisons. Those
+elements that were not discarded are returned.
 
-This can be used to remove elements from an array where a “better” element, in some partial
-order, exists in the array.
+This can be used to remove elements from an array where a “better” element, in some partial order,
+exists in the array.
+
+Example:
+```lean example
+#eval #["a", "r", "red", "x", "r"].filterPairsM fun x y =>
+  pure (!(x.isPrefixOf y), true)
+```
+```output
+#["a", "red", "x", "r"]
+```
 -/
 def filterPairsM {m} [Monad m] {α} (a : Array α) (f : α → α → m (Bool × Bool)) :
     m (Array α) := do

src/Std/Data/HashMap/Basic.lean

@@ -289,8 +289,16 @@ end Unverified
 end Std.HashMap
 
 /--
-Groups all elements `x`, `y` in `xs` with `key x == key y` into the same array
-`(xs.groupByKey key).find! (key x)`. Groups preserve the relative order of elements in `xs`.
+Groups the elements of an array `xs` according to the function `key`, returning a hash map in which
+each group is associated with its key. Groups preserve the relative order of elements in `xs`.
+
+Example:
+```lean example
+#eval #[0, 1, 2, 3, 4, 5, 6].groupByKey (· % 2)
+```
+```output
+Std.HashMap.ofList [(0, #[0, 2, 4, 6]), (1, #[1, 3, 5])]
+```
 -/
 def Array.groupByKey [BEq α] [Hashable α] (key : β → α) (xs : Array β)
     : Std.HashMap α (Array β) := Id.run do

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

@@ -639,7 +639,7 @@
   "end": {"line": 297, "character": 29}},
  "contents":
  {"value":
-  "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\nCombines two lists into a list of pairs in which the first and second components are the\ncorresponding elements of each list. The resulting list is the length of the shorter of the inputs\nlists.\n\n`O(min |xs| |ys|)`.\n\nExamples:\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2, 3] = [(\"Mon\", 1), (\"Tue\", 2), (\"Wed\", 3)]`\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2] = [(\"Mon\", 1), (\"Tue\", 2)]`\n* `[x₁, x₂, x₃].zip [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*",
+  "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\nCombines two lists into a list of pairs in which the first and second components are the\ncorresponding elements of each list. The resulting list is the length of the shorter of the input\nlists.\n\n`O(min |xs| |ys|)`.\n\nExamples:\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2, 3] = [(\"Mon\", 1), (\"Tue\", 2), (\"Wed\", 3)]`\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2] = [(\"Mon\", 1), (\"Tue\", 2)]`\n* `[x₁, x₂, x₃].zip [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 297, "character": 19}}
@@ -648,5 +648,5 @@
   "end": {"line": 297, "character": 22}},
  "contents":
  {"value":
-  "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\nCombines two lists into a list of pairs in which the first and second components are the\ncorresponding elements of each list. The resulting list is the length of the shorter of the inputs\nlists.\n\n`O(min |xs| |ys|)`.\n\nExamples:\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2, 3] = [(\"Mon\", 1), (\"Tue\", 2), (\"Wed\", 3)]`\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2] = [(\"Mon\", 1), (\"Tue\", 2)]`\n* `[x₁, x₂, x₃].zip [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*",
+  "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\nCombines two lists into a list of pairs in which the first and second components are the\ncorresponding elements of each list. The resulting list is the length of the shorter of the input\nlists.\n\n`O(min |xs| |ys|)`.\n\nExamples:\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2, 3] = [(\"Mon\", 1), (\"Tue\", 2), (\"Wed\", 3)]`\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2] = [(\"Mon\", 1), (\"Tue\", 2)]`\n* `[x₁, x₂, x₃].zip [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*",
   "kind": "markdown"}}