update doc-string

src/Init/Data/Array/Basic.lean

@@ -254,7 +254,7 @@ instance [BEq α] : BEq (Array α) :=
 ```
 ofFn f = #[f 0, f 1, ... , f(n - 1)]
 ``` -/
-def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
+def ofFn {n} (f : Fin n → α) : Array α := go 0 (emptyWithCapacity n) where
   /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
   @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   go (i : Nat) (acc : Array α) : Array α :=
@@ -505,7 +505,7 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
       else
         pure bs
   decreasing_by simp_wf; decreasing_trivial_pre_omega
-  map 0 (mkEmpty as.size)
+  map 0 (emptyWithCapacity as.size)
 
 @[deprecated mapM (since := "2024-11-11")] abbrev sequenceMap := @mapM
 
@@ -522,7 +522,7 @@ def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
         apply Nat.le_add_right
       have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
       map i (j+1) this (bs.push (← f j as[j] j_lt))
-  map as.size 0 rfl (mkEmpty as.size)
+  map as.size 0 rfl (emptyWithCapacity as.size)
 
 @[inline]
 def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) : m (Array β) :=

src/Init/Data/Array/Lemmas.lean

@@ -57,7 +57,10 @@ theorem toArray_eq : List.toArray as = xs ↔ as = xs.toList := by
 
 theorem size_empty : (#[] : Array α).size = 0 := rfl
 
-@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
+@[simp] theorem emptyWithCapacity_eq (α n) : @emptyWithCapacity α n = #[] := rfl
+
+@[deprecated emptyWithCapacity_eq (since := "2025-03-12")]
+theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
 
 /-! ### size -/
 
@@ -2655,7 +2658,7 @@ theorem extract_loop_eq_aux (xs ys : Array α) (size start : Nat) :
 
 theorem extract_loop_eq (xs ys : Array α) (size start : Nat) (h : start + size ≤ xs.size) :
   extract.loop xs size start ys = ys ++ xs.extract start (start + size) := by
-  simp only [extract, Nat.sub_eq, mkEmpty_eq]
+  simp only [extract, Nat.sub_eq, emptyWithCapacity_eq]
   rw [extract_loop_eq_aux, Nat.min_eq_left h, Nat.add_sub_cancel_left]
 
 theorem size_extract_loop (xs ys : Array α) (size start : Nat) :
@@ -2672,7 +2675,7 @@ theorem size_extract_loop (xs ys : Array α) (size start : Nat) :
 
 @[simp] theorem size_extract (xs : Array α) (start stop : Nat) :
     (xs.extract start stop).size = min stop xs.size - start := by
-  simp only [extract, Nat.sub_eq, mkEmpty_eq]
+  simp only [extract, Nat.sub_eq, emptyWithCapacity_eq]
   rw [size_extract_loop, size_empty, Nat.zero_add, Nat.sub_min_sub_right, Nat.min_assoc,
     Nat.min_self]
 
@@ -2775,12 +2778,12 @@ abbrev extract_all := @extract_size
 
 theorem extract_empty_of_stop_le_start (xs : Array α) {start stop : Nat} (h : stop ≤ start) :
     xs.extract start stop = #[] := by
-  simp only [extract, Nat.sub_eq, mkEmpty_eq]
+  simp only [extract, Nat.sub_eq, emptyWithCapacity_eq]
   rw [←Nat.sub_min_sub_right, Nat.sub_eq_zero_of_le h, Nat.zero_min, extract_loop_zero]
 
 theorem extract_empty_of_size_le_start (xs : Array α) {start stop : Nat} (h : xs.size ≤ start) :
     xs.extract start stop = #[] := by
-  simp only [extract, Nat.sub_eq, mkEmpty_eq]
+  simp only [extract, Nat.sub_eq, emptyWithCapacity_eq]
   rw [←Nat.sub_min_sub_right, Nat.sub_eq_zero_of_le h, Nat.min_zero, extract_loop_zero]
 
 @[simp] theorem extract_empty (start stop : Nat) : (#[] : Array α).extract start stop = #[] :=

src/Init/Data/ByteArray/Basic.lean

@@ -18,10 +18,13 @@ attribute [extern "lean_byte_array_data"] ByteArray.data
 
 namespace ByteArray
 @[extern "lean_mk_empty_byte_array"]
-def mkEmpty (c : @& Nat) : ByteArray :=
+def emptyWithCapacity (c : @& Nat) : ByteArray :=
   { data := #[] }
 
-def empty : ByteArray := mkEmpty 0
+@[deprecated emptyWithCapacity (since := "2025-03-12")]
+abbrev mkEmpty := emptyWithCapacity
+
+def empty : ByteArray := emptyWithCapacity 0
 
 instance : Inhabited ByteArray where
   default := empty

src/Init/Data/FloatArray/Basic.lean

@@ -17,11 +17,14 @@ attribute [extern "lean_float_array_data"] FloatArray.data
 
 namespace FloatArray
 @[extern "lean_mk_empty_float_array"]
-def mkEmpty (c : @& Nat) : FloatArray :=
+def emptyWithCapacity (c : @& Nat) : FloatArray :=
   { data := #[] }
 
+@[deprecated emptyWithCapacity (since := "2025-03-12")]
+abbrev mkEmpty := emptyWithCapacity
+
 def empty : FloatArray :=
-  mkEmpty 0
+  emptyWithCapacity 0
 
 instance : Inhabited FloatArray where
   default := empty

src/Init/Data/Vector/Basic.lean

@@ -59,7 +59,10 @@ def elimAsList {motive : Vector α n → Sort u}
   | ⟨⟨xs⟩, ha⟩ => mk xs ha
 
 /-- Make an empty vector with pre-allocated capacity. -/
-@[inline] def mkEmpty (capacity : Nat) : Vector α 0 := ⟨.mkEmpty capacity, rfl⟩
+@[inline] def emptyWithCapacity (capacity : Nat) : Vector α 0 := ⟨.mkEmpty capacity, rfl⟩
+
+@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity]
+abbrev mkEmpty := @emptyWithCapacity
 
 /-- Makes a vector of size `n` with all cells containing `v`. -/
 @[inline] def mkVector (n) (v : α) : Vector α n := ⟨mkArray n v, by simp⟩

src/Init/Data/Vector/Lemmas.lean

@@ -277,8 +277,11 @@ abbrev zipWithIndex_mk := @zipIdx_mk
 
 @[simp] theorem toArray_empty : (#v[] : Vector α 0).toArray = #[] := rfl
 
-@[simp] theorem toArray_mkEmpty (cap) :
-    (Vector.mkEmpty (α := α) cap).toArray = Array.mkEmpty cap := rfl
+@[simp] theorem toArray_emptyWithCapacity (cap) :
+    (Vector.emptyWithCapacity (α := α) cap).toArray = Array.emptyWithCapacity cap := rfl
+
+@[deprecated toArray_emptyWithCapacity (since := "2025-03-12")]
+abbrev toArray_mkEmpty := @toArray_emptyWithCapacity
 
 @[simp] theorem toArray_eraseIdx (xs : Vector α n) (i) (h) :
     (xs.eraseIdx i h).toArray = xs.toArray.eraseIdx i (by simp [h]) := rfl
@@ -509,8 +512,11 @@ theorem toList_append (xs : Vector α m) (ys : Vector α n) :
 
 theorem toList_empty : (#v[] : Vector α 0).toArray = #[] := by simp
 
-theorem toList_mkEmpty (cap) :
-    (Vector.mkEmpty (α := α) cap).toList = [] := rfl
+theorem toList_emptyWithCapacity (cap) :
+    (Vector.emptyWithCapacity (α := α) cap).toList = [] := rfl
+
+@[deprecated toList_emptyWithCapacity (since := "2025-03-12")]
+abbrev toList_mkEmpty := @toList_emptyWithCapacity
 
 theorem toList_eraseIdx (xs : Vector α n) (i) (h) :
     (xs.eraseIdx i h).toList = xs.toList.eraseIdx i := by simp

src/Init/Prelude.lean

@@ -2658,7 +2658,7 @@ array, so it has comparable performance 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.mkEmpty n` creates an array which is equal to `#[]`,
+is not observable from Lean code. `Array.emptyWithCapacity n` creates an array which is equal to `#[]`,
 but internally allocates an array of capacity `n`.
 
 From the point of view of proofs `Array α` is just a wrapper around `List α`.
@@ -2692,13 +2692,22 @@ list.
 @[match_pattern]
 abbrev List.toArray (xs : List α) : Array α := .mk xs
 
-/-- Construct a new empty array with initial capacity `c`. -/
+/-- Construct a new empty array with initial capacity `c`.
+
+This will be deprecated in favor of `Array.emptyWithCapacity` in the future.
+-/
 @[extern "lean_mk_empty_array_with_capacity"]
 def Array.mkEmpty {α : Type u} (c : @& Nat) : Array α where
   toList := List.nil
 
+
+set_option linter.unusedVariables false in
+/-- Construct 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. -/
-def Array.empty {α : Type u} : Array α := mkEmpty 0
+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. -/
 @[reducible, extern "lean_array_get_size"]
@@ -2742,39 +2751,39 @@ def Array.push {α : Type u} (a : Array α) (v : α) : Array α where
 
 /-- Create array `#[]` -/
 def Array.mkArray0 {α : Type u} : Array α :=
-  mkEmpty 0
+  emptyWithCapacity 0
 
 /-- Create array `#[a₁]` -/
 def Array.mkArray1 {α : Type u} (a₁ : α) : Array α :=
-  (mkEmpty 1).push a₁
+  (emptyWithCapacity 1).push a₁
 
 /-- Create array `#[a₁, a₂]` -/
 def Array.mkArray2 {α : Type u} (a₁ a₂ : α) : Array α :=
-  ((mkEmpty 2).push a₁).push a₂
+  ((emptyWithCapacity 2).push a₁).push a₂
 
 /-- Create array `#[a₁, a₂, a₃]` -/
 def Array.mkArray3 {α : Type u} (a₁ a₂ a₃ : α) : Array α :=
-  (((mkEmpty 3).push a₁).push a₂).push a₃
+  (((emptyWithCapacity 3).push a₁).push a₂).push a₃
 
 /-- Create array `#[a₁, a₂, a₃, a₄]` -/
 def Array.mkArray4 {α : Type u} (a₁ a₂ a₃ a₄ : α) : Array α :=
-  ((((mkEmpty 4).push a₁).push a₂).push a₃).push a₄
+  ((((emptyWithCapacity 4).push a₁).push a₂).push a₃).push a₄
 
 /-- Create array `#[a₁, a₂, a₃, a₄, a₅]` -/
 def Array.mkArray5 {α : Type u} (a₁ a₂ a₃ a₄ a₅ : α) : Array α :=
-  (((((mkEmpty 5).push a₁).push a₂).push a₃).push a₄).push a₅
+  (((((emptyWithCapacity 5).push a₁).push a₂).push a₃).push a₄).push a₅
 
 /-- Create array `#[a₁, a₂, a₃, a₄, a₅, a₆]` -/
 def Array.mkArray6 {α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ : α) : Array α :=
-  ((((((mkEmpty 6).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆
+  ((((((emptyWithCapacity 6).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆
 
 /-- Create array `#[a₁, a₂, a₃, a₄, a₅, a₆, a₇]` -/
 def Array.mkArray7 {α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ a₇ : α) : Array α :=
-  (((((((mkEmpty 7).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆).push a₇
+  (((((((emptyWithCapacity 7).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆).push a₇
 
 /-- Create array `#[a₁, a₂, a₃, a₄, a₅, a₆, a₇, a₈]` -/
 def Array.mkArray8 {α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : α) : Array α :=
-  ((((((((mkEmpty 8).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆).push a₇).push a₈
+  ((((((((emptyWithCapacity 8).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆).push a₇).push a₈
 
 /-- Slower `Array.append` used in quotations. -/
 protected def Array.appendCore {α : Type u}  (as : Array α) (bs : Array α) : Array α :=
@@ -2801,7 +2810,7 @@ def Array.extract (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : A
         | Nat.succ i' => loop i' (hAdd j 1) (bs.push (as.getInternal j hlt)))
       (fun _ => bs)
   let sz' := Nat.sub (min stop as.size) start
-  loop sz' start (mkEmpty sz')
+  loop sz' start (emptyWithCapacity sz')
 
 /-- The typeclass which supplies the `>>=` "bind" function. See `Monad`. -/
 class Bind (m : Type u → Type v) where

src/Init/System/IO.lean

@@ -645,7 +645,7 @@ def readBinFile (fname : FilePath) : IO ByteArray := do
     if size > 0 then
       handle.read mdata.byteSize.toUSize
     else
-      pure <| ByteArray.mkEmpty 0
+      pure <| ByteArray.emptyWithCapacity 0
   handle.readBinToEndInto buf
 
 def readFile (fname : FilePath) : IO String := do

src/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean

@@ -79,7 +79,7 @@ def run (proof : Array IntAction) (x : M α) : Except String α := do
     | .addEmpty id .. | .addRup id .. | .addRat id .. => acc.insert id a
     | .del .. => acc
   let proof := proof.foldl (init := {}) folder
-  let used := Nat.fold proof.size (init := ByteArray.mkEmpty proof.size) (fun _ _ acc => acc.push 0)
+  let used := Nat.fold proof.size (init := ByteArray.emptyWithCapacity proof.size) (fun _ _ acc => acc.push 0)
   let mapped := Array.mkArray proof.size 0
   return ReaderT.run x { proof, initialId, addEmptyId } |>.run' { used, mapped }
 

src/Std/Tactic/BVDecide/LRAT/Parser.lean

@@ -332,7 +332,7 @@ Serialize `proof` into the binary LRAT format as a `ByteArray`.
 -/
 partial def lratProofToBinary (proof : Array IntAction) : ByteArray :=
   -- we will definitely need at least 4 bytes per add step and almost exclusively produce add.
-  go 0 (ByteArray.mkEmpty (4 * proof.size))
+  go 0 (ByteArray.emptyWithCapacity (4 * proof.size))
 where
   go (idx : Nat) (acc : ByteArray) : ByteArray :=
     if h : idx < proof.size then