feat: deprecate Array.mkArray in favour of Array.replicate

This PR fixes a bug introduced in #7589, causing pretty printed
structure instances to not be hoverable in the Infoview.

This was caused by a choice node being introduced, since `{ $fields,* }`
is ambiguous syntax.

.github/workflows/awaiting-mathlib.yml

@@ -3,7 +3,7 @@ name: Check awaiting-mathlib label
 on:
   merge_group:
   pull_request:
-    types: [opened, labeled]
+    types: [opened, synchronize, reopened, labeled, unlabeled]
 
 jobs:
   check-awaiting-mathlib:
@@ -17,4 +17,4 @@ jobs:
             const { labels } = context.payload.pull_request;
             if (labels.some(label => label.name == "awaiting-mathlib") && !labels.some(label => label.name == "builds-mathlib")) {
               core.setFailed('PR is marked "awaiting-mathlib" but "builds-mathlib" label has not been applied yet by the bot');
-            }
+            }

.github/workflows/build-template.yml

@@ -72,6 +72,9 @@ jobs:
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
+      - name: Open Nix shell once
+        run: true
+        if: runner.os == 'Linux'
       # Do check out some CI-relevant files from virtual merge commit to accommodate CI changes on
       # master (as the workflow files themselves are always taken from the merge)
       # (needs to be after "Install *" to use the right shell)
@@ -130,6 +133,7 @@ jobs:
           echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
       - name: Build
         run: |
+          ulimit -c unlimited  # coredumps
           [ -d build ] || mkdir build
           cd build
           # arguments passed to `cmake`
@@ -197,6 +201,7 @@ jobs:
       - name: Test
         id: test
         run: |
+          ulimit -c unlimited  # coredumps
           time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
         if: (matrix.wasm || !matrix.cross) && inputs.check-level >= 1
       - name: Test Summary
@@ -232,3 +237,10 @@ jobs:
         if: matrix.name == 'Linux' && inputs.check-level >= 1
       - name: CCache stats
         run: ccache -s
+      - name: Show stacktrace for coredumps
+        if: failure() && runner.os == 'Linux'
+        run: |
+          for c in $(find . -name core); do
+            progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
+            echo bt | $GDB/bin/gdb -q $progbin $c || true
+          done

.github/workflows/ci.yml

@@ -300,6 +300,7 @@ jobs:
   # build jobs that should not be considered by `all-done` below
   build-secondary:
     needs: [configure]
+    if: needs.configure.outputs.matrix-secondary != '[]'
     uses: ./.github/workflows/build-template.yml
     with:
       config: ${{needs.configure.outputs.matrix-secondary}}

flake.nix

@@ -63,6 +63,7 @@
           GLIBC_DEV = pkgsDist.glibc.dev;
           GCC_LIB = pkgsDist.gcc.cc.lib;
           ZLIB = pkgsDist.zlib;
+          # for CI coredumps
           GDB = pkgsDist.gdb;
         });
     in {

src/Init/Control/Basic.lean

@@ -135,6 +135,13 @@ instance : ToBool Bool where
   | true  => t
   | false => f
 
+/--
+Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns it and ignores
+`y`; otherwise, runs `y` and returns its result.
+
+This a monadic counterpart to the short-circuiting `||` operator, usually accessed via the `<||>`
+operator.
+-/
 @[macro_inline] def orM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
   let b ← x
   match toBool b with
@@ -145,6 +152,13 @@ infixr:30 " <||> " => orM
 
 recommended_spelling "orM" for "<||>" in [orM, «term_<||>_»]
 
+/--
+Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns `y`; otherwise,
+returns the original result of `x`.
+
+This a monadic counterpart to the short-circuiting `&&` operator, usually accessed via the `<&&>`
+operator.
+-/
 @[macro_inline] def andM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
   let b ← x
   match toBool b with
@@ -155,6 +169,9 @@ infixr:35 " <&&> " => andM
 
 recommended_spelling "andM" for "<&&>" in [andM, «term_<&&>_»]
 
+/--
+Runs a monadic action and returns the negation of its result.
+-/
 @[macro_inline] def notM {m : Type → Type v} [Applicative m] (x : m Bool) : m Bool :=
   not <$> x
 

src/Init/Control/Except.lean

@@ -265,13 +265,24 @@ instance (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (Excep
   liftWith f := liftM <| f fun x => x.run
   restoreM x := x
 
+/--
+Monads that provide the ability to ensure an action happens, regardless of exceptions or other
+failures.
+
+`MonadFinally.tryFinally'` is used to desugar `try ... finally ...` syntax.
+-/
 class MonadFinally (m : Type u → Type v) where
-  /-- `tryFinally' x f` runs `x` and then the "finally" computation `f`.
-  When `x` succeeds with `a : α`, `f (some a)` is returned. If `x` fails
-  for `m`'s definition of failure, `f none` is returned. Hence `tryFinally'`
-  can be thought of as performing the same role as a `finally` block in
-  an imperative programming language. -/
-  tryFinally' {α β} : m α → (Option α → m β) → m (α × β)
+  /--
+  Runs an action, ensuring that some other action always happens afterward.
+
+  More specifically, `tryFinally' x f` runs `x` and then the “finally” computation `f`. If `x`
+  succeeds with some value `a : α`, `f (some a)` is returned. If `x` fails for `m`'s definition of
+  failure, `f none` is returned.
+
+  `tryFinally'` can be thought of as performing the same role as a `finally` block in an imperative
+  programming language.
+  -/
+  tryFinally' {α β} : (x : m α) → (f : Option α → m β) → m (α × β)
 
 export MonadFinally (tryFinally')
 

src/Init/Core.lean

@@ -865,37 +865,55 @@ noncomputable def HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : S
 noncomputable def HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : HEq a b) (h₂ : p a) : p b :=
   eq_of_heq h₁ ▸ h₂
 
+/-- Substitution with heterogeneous equality. -/
 theorem HEq.subst {p : (T : Sort u) → T → Prop} (h₁ : HEq a b) (h₂ : p α a) : p β b :=
   HEq.ndrecOn h₁ h₂
 
+/-- Heterogeneous equality is symmetric. -/
 @[symm] theorem HEq.symm (h : HEq a b) : HEq b a :=
   h.rec (HEq.refl a)
 
+/-- Propositionally equal terms are also heterogeneously equal. -/
 theorem heq_of_eq (h : a = a') : HEq a a' :=
   Eq.subst h (HEq.refl a)
 
+/-- Heterogeneous equality is transitive. -/
 theorem HEq.trans (h₁ : HEq a b) (h₂ : HEq b c) : HEq a c :=
   HEq.subst h₂ h₁
 
+/-- Heterogeneous equality precomposes with propositional equality. -/
 theorem heq_of_heq_of_eq (h₁ : HEq a b) (h₂ : b = b') : HEq a b' :=
   HEq.trans h₁ (heq_of_eq h₂)
 
+/-- Heterogeneous equality postcomposes with propositional equality. -/
 theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : HEq a' b) : HEq a b :=
   HEq.trans (heq_of_eq h₁) h₂
 
+/-- If two terms are heterogeneously equal then their types are propositionally equal. -/
 theorem type_eq_of_heq (h : HEq a b) : α = β :=
   h.rec (Eq.refl α)
 
 end
 
+/--
+Rewriting inside `φ` using `Eq.recOn` yields a term that's heterogeneously equal to the original
+term.
+-/
 theorem eqRec_heq {α : Sort u} {φ : α → Sort v} {a a' : α} : (h : a = a') → (p : φ a) → HEq (Eq.recOn (motive := fun x _ => φ x) h p) p
   | rfl, p => HEq.refl p
 
+/--
+If casting a term with `Eq.rec` to another type makes it equal to some other term, then the two
+terms are heterogeneously equal.
+-/
 theorem heq_of_eqRec_eq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : Eq.rec (motive := fun α _ => α) a h₁ = b) : HEq a b := by
   subst h₁
   apply heq_of_eq
   exact h₂
 
+/--
+The result of casting a term with `cast` is heterogeneously equal to the original term.
+-/
 theorem cast_heq {α β : Sort u} : (h : α = β) → (a : α) → HEq (cast h a) a
   | rfl, a => HEq.refl a
 

src/Init/Data/Array/Attach.lean

@@ -743,10 +743,13 @@ and simplifies these to the function directly taking the value.
     List.map_toArray, List.map_flatten, map_subtype, map_id_fun', List.unattach_toArray, mk.injEq]
   simp only [List.unattach]
 
-@[simp] theorem unattach_mkArray {p : α → Prop} {n : Nat} {x : { x // p x }} :
-    (Array.mkArray n x).unattach = Array.mkArray n x.1 := by
+@[simp] theorem unattach_replicate {p : α → Prop} {n : Nat} {x : { x // p x }} :
+    (Array.replicate n x).unattach = Array.replicate n x.1 := by
   simp [unattach]
 
+@[deprecated unattach_replicate (since := "2025-03-18")]
+abbrev unattach_mkArray := @unattach_replicate
+
 /-! ### Well-founded recursion preprocessing setup -/
 
 @[wf_preprocess] theorem Array.map_wfParam (xs : Array α) (f : α → β) :

src/Init/Data/Array/Basic.lean

@@ -202,12 +202,26 @@ Creates an array that contains `n` repetitions of `v`.
 
 The corresponding `List` function is `List.replicate`.
 
+Examples:
+ * `Array.replicate 2 true = #[true, true]`
+ * `Array.replicate 3 () = #[(), (), ()]`
+ * `Array.replicate 0 "anything" = #[]`
+-/
+@[extern "lean_mk_array"]
+def replicate {α : Type u} (n : Nat) (v : α) : Array α where
+  toList := List.replicate n v
+
+/--
+Creates an array that contains `n` repetitions of `v`.
+
+The corresponding `List` function is `List.replicate`.
+
 Examples:
  * `Array.mkArray 2 true = #[true, true]`
  * `Array.mkArray 3 () = #[(), (), ()]`
  * `Array.mkArray 0 "anything" = #[]`
 -/
-@[extern "lean_mk_array"]
+@[extern "lean_mk_array", deprecated replicate (since := "2025-03-18")]
 def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
   toList := List.replicate n v
 
@@ -748,7 +762,10 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
 
 @[deprecated mapM (since := "2024-11-11")] abbrev sequenceMap := @mapM
 
-/-- Variant of `mapIdxM` which receives the index `i` along with the bound `i < as.size`. -/
+/--
+Applies the monadic action `f` to every element in the array, along with the element's index and a
+proof that the index is in bounds, from left to right. Returns the array of results.
+-/
 @[inline]
 def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
     (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → m β) : m (Array β) :=
@@ -763,6 +780,10 @@ def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
       map i (j+1) this (bs.push (← f j as[j] j_lt))
   map as.size 0 rfl (emptyWithCapacity as.size)
 
+/--
+Applies the monadic action `f` to every element in the array, along with the element's index, from
+left to right. Returns the array of results.
+-/
 @[inline]
 def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) : m (Array β) :=
   as.mapFinIdxM fun i a _ => f i a
@@ -2049,7 +2070,7 @@ Examples:
  * `#["red", "green", "blue"].leftpad 3 "blank" = #["red", "green", "blue"]`
  * `#["red", "green", "blue"].leftpad 1 "blank" = #["red", "green", "blue"]`
 -/
-def leftpad (n : Nat) (a : α) (xs : Array α) : Array α := mkArray (n - xs.size) a ++ xs
+def leftpad (n : Nat) (a : α) (xs : Array α) : Array α := replicate (n - xs.size) a ++ xs
 
 /--
 Pads `xs : Array α` on the right with repeated occurrences of `a : α` until it is of length `n`. If
@@ -2061,7 +2082,7 @@ Examples:
  * `#["red", "green", "blue"].rightpad 3 "blank" = #["red", "green", "blue"]`
  * `#["red", "green", "blue"].rightpad 1 "blank" = #["red", "green", "blue"]`
 -/
-def rightpad (n : Nat) (a : α) (xs : Array α) : Array α := xs ++ mkArray (n - xs.size) a
+def rightpad (n : Nat) (a : α) (xs : Array α) : Array α := xs ++ replicate (n - xs.size) a
 
 /- ### reduceOption -/
 

src/Init/Data/Array/Count.lean

@@ -88,10 +88,13 @@ theorem countP_le_size : countP p xs ≤ xs.size := by
   rcases xs with ⟨xs⟩
   simp
 
-theorem countP_mkArray (p : α → Bool) (a : α) (n : Nat) :
-    countP p (mkArray n a) = if p a then n else 0 := by
+theorem countP_replicate (p : α → Bool) (a : α) (n : Nat) :
+    countP p (replicate n a) = if p a then n else 0 := by
   simp [← List.toArray_replicate, List.countP_replicate]
 
+@[deprecated countP_replicate (since := "2025-03-18")]
+abbrev countP_mkArray := @countP_replicate
+
 theorem boole_getElem_le_countP (p : α → Bool) (xs : Array α) (i : Nat) (h : i < xs.size) :
     (if p xs[i] then 1 else 0) ≤ xs.countP p := by
   rcases xs with ⟨xs⟩
@@ -241,25 +244,34 @@ theorem count_eq_size {xs : Array α} : count a xs = xs.size ↔ ∀ b ∈ xs, a
   · simpa using h b hb
   · rw [h b hb, beq_self_eq_true]
 
-@[simp] theorem count_mkArray_self (a : α) (n : Nat) : count a (mkArray n a) = n := by
+@[simp] theorem count_replicate_self (a : α) (n : Nat) : count a (replicate n a) = n := by
   simp [← List.toArray_replicate]
 
-theorem count_mkArray (a b : α) (n : Nat) : count a (mkArray n b) = if b == a then n else 0 := by
+@[deprecated count_replicate_self (since := "2025-03-18")]
+abbrev count_mkArray_self := @count_replicate_self
+
+theorem count_replicate (a b : α) (n : Nat) : count a (replicate n b) = if b == a then n else 0 := by
   simp [← List.toArray_replicate, List.count_replicate]
 
-theorem filter_beq (xs : Array α) (a : α) : xs.filter (· == a) = mkArray (count a xs) a := by
+@[deprecated count_replicate (since := "2025-03-18")]
+abbrev count_mkArray := @count_replicate
+
+theorem filter_beq (xs : Array α) (a : α) : xs.filter (· == a) = replicate (count a xs) a := by
   rcases xs with ⟨xs⟩
   simp [List.filter_beq]
 
-theorem filter_eq {α} [DecidableEq α] (xs : Array α) (a : α) : xs.filter (· = a) = mkArray (count a xs) a :=
+theorem filter_eq {α} [DecidableEq α] (xs : Array α) (a : α) : xs.filter (· = a) = replicate (count a xs) a :=
   filter_beq xs a
 
-theorem mkArray_count_eq_of_count_eq_size {xs : Array α} (h : count a xs = xs.size) :
-    mkArray (count a xs) a = xs := by
+theorem replicate_count_eq_of_count_eq_size {xs : Array α} (h : count a xs = xs.size) :
+    replicate (count a xs) a = xs := by
   rcases xs with ⟨xs⟩
   rw [← toList_inj]
   simp [List.replicate_count_eq_of_count_eq_length (by simpa using h)]
 
+@[deprecated replicate_count_eq_of_count_eq_size (since := "2025-03-18")]
+abbrev mkArray_count_eq_of_count_eq_size := @replicate_count_eq_of_count_eq_size
+
 @[simp] theorem count_filter {xs : Array α} (h : p a) : count a (filter p xs) = count a xs := by
   rcases xs with ⟨xs⟩
   simp [List.count_filter, h]

src/Init/Data/Array/Erase.lean

@@ -122,21 +122,30 @@ theorem eraseP_append {xs : Array α} {ys : Array α} :
   simp only [List.append_toArray, List.eraseP_toArray, List.eraseP_append, List.any_toArray]
   split <;> simp
 
-theorem eraseP_mkArray (n : Nat) (a : α) (p : α → Bool) :
-    (mkArray n a).eraseP p = if p a then mkArray (n - 1) a else mkArray n a := by
+theorem eraseP_replicate (n : Nat) (a : α) (p : α → Bool) :
+    (replicate n a).eraseP p = if p a then replicate (n - 1) a else replicate n a := by
   simp only [← List.toArray_replicate, List.eraseP_toArray, List.eraseP_replicate]
   split <;> simp
 
-@[simp] theorem eraseP_mkArray_of_pos {n : Nat} {a : α} (h : p a) :
-    (mkArray n a).eraseP p = mkArray (n - 1) a := by
+@[deprecated eraseP_replicate (since := "2025-03-18")]
+abbrev eraseP_mkArray := @eraseP_replicate
+
+@[simp] theorem eraseP_replicate_of_pos {n : Nat} {a : α} (h : p a) :
+    (replicate n a).eraseP p = replicate (n - 1) a := by
   simp only [← List.toArray_replicate, List.eraseP_toArray]
   simp [h]
 
-@[simp] theorem eraseP_mkArray_of_neg {n : Nat} {a : α} (h : ¬p a) :
-    (mkArray n a).eraseP p = mkArray n a := by
+@[deprecated eraseP_replicate_of_pos (since := "2025-03-18")]
+abbrev eraseP_mkArray_of_pos := @eraseP_replicate_of_pos
+
+@[simp] theorem eraseP_replicate_of_neg {n : Nat} {a : α} (h : ¬p a) :
+    (replicate n a).eraseP p = replicate n a := by
   simp only [← List.toArray_replicate, List.eraseP_toArray]
   simp [h]
 
+@[deprecated eraseP_replicate_of_neg (since := "2025-03-18")]
+abbrev eraseP_mkArray_of_neg := @eraseP_replicate_of_neg
+
 theorem eraseP_eq_iff {p} {xs : Array α} :
     xs.eraseP p = ys ↔
       ((∀ a ∈ xs, ¬ p a) ∧ xs = ys) ∨
@@ -243,12 +252,15 @@ theorem erase_append [LawfulBEq α] {a : α} {xs ys : Array α} :
   simp only [List.append_toArray, List.erase_toArray, List.erase_append, mem_toArray]
   split <;> simp
 
-theorem erase_mkArray [LawfulBEq α] (n : Nat) (a b : α) :
-    (mkArray n a).erase b = if b == a then mkArray (n - 1) a else mkArray n a := by
+theorem erase_replicate [LawfulBEq α] (n : Nat) (a b : α) :
+    (replicate n a).erase b = if b == a then replicate (n - 1) a else replicate n a := by
   simp only [← List.toArray_replicate, List.erase_toArray]
   simp only [List.erase_replicate, beq_iff_eq, List.toArray_replicate]
   split <;> simp
 
+@[deprecated erase_replicate (since := "2025-03-18")]
+abbrev erase_mkArray := @erase_replicate
+
 theorem erase_comm [LawfulBEq α] (a b : α) (xs : Array α) :
     (xs.erase a).erase b = (xs.erase b).erase a := by
   rcases xs with ⟨xs⟩
@@ -268,16 +280,22 @@ theorem erase_eq_iff [LawfulBEq α] {a : α} {xs : Array α} :
     · left; simp_all
     · right; refine ⟨a, as, h, rfl, bs, by simp⟩
 
-@[simp] theorem erase_mkArray_self [LawfulBEq α] {a : α} :
-    (mkArray n a).erase a = mkArray (n - 1) a := by
+@[simp] theorem erase_replicate_self [LawfulBEq α] {a : α} :
+    (replicate n a).erase a = replicate (n - 1) a := by
   simp only [← List.toArray_replicate, List.erase_toArray]
   simp [List.erase_replicate]
 
-@[simp] theorem erase_mkArray_ne [LawfulBEq α] {a b : α} (h : !b == a) :
-    (mkArray n a).erase b = mkArray n a := by
+@[deprecated erase_replicate_self (since := "2025-03-18")]
+abbrev erase_mkArray_self := @erase_replicate_self
+
+@[simp] theorem erase_replicate_ne [LawfulBEq α] {a b : α} (h : !b == a) :
+    (replicate n a).erase b = replicate n a := by
   rw [erase_of_not_mem]
   simp_all
 
+@[deprecated erase_replicate_ne (since := "2025-03-18")]
+abbrev erase_mkArray_ne := @erase_replicate_ne
+
 end erase
 
 /-! ### eraseIdx -/
@@ -353,12 +371,15 @@ theorem eraseIdx_append_of_length_le {xs : Array α} {k : Nat} (hk : xs.size ≤
   simp at hk
   simp [List.eraseIdx_append_of_length_le, *]
 
-theorem eraseIdx_mkArray {n : Nat} {a : α} {k : Nat} {h} :
-    (mkArray n a).eraseIdx k = mkArray (n - 1) a := by
+theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} {h} :
+    (replicate n a).eraseIdx k = replicate (n - 1) a := by
   simp at h
   simp only [← List.toArray_replicate, List.eraseIdx_toArray]
   simp [List.eraseIdx_replicate, h]
 
+@[deprecated eraseIdx_replicate (since := "2025-03-18")]
+abbrev eraseIdx_mkArray := @eraseIdx_replicate
+
 theorem mem_eraseIdx_iff_getElem {x : α} {xs : Array α} {k} {h} : x ∈ xs.eraseIdx k h ↔ ∃ i w, i ≠ k ∧ xs[i]'w = x := by
   rcases xs with ⟨xs⟩
   simp [List.mem_eraseIdx_iff_getElem, *]

src/Init/Data/Array/Extract.lean

@@ -249,12 +249,15 @@ theorem extract_append_left {as bs : Array α} :
   · simp only [size_map, size_extract] at h₁ h₂
     simp only [getElem_map, getElem_extract]
 
-@[simp] theorem extract_mkArray {a : α} {n i j : Nat} :
-    (mkArray n a).extract i j = mkArray (min j n - i) a := by
+@[simp] theorem extract_replicate {a : α} {n i j : Nat} :
+    (replicate n a).extract i j = replicate (min j n - i) a := by
   ext l h₁ h₂
   · simp
-  · simp only [size_extract, size_mkArray] at h₁ h₂
-    simp only [getElem_extract, getElem_mkArray]
+  · simp only [size_extract, size_replicate] at h₁ h₂
+    simp only [getElem_extract, getElem_replicate]
+
+@[deprecated extract_replicate (since := "2025-03-18")]
+abbrev extract_mkArray := @extract_replicate
 
 theorem extract_eq_extract_right {as : Array α} {i j j' : Nat} :
     as.extract i j = as.extract i j' ↔ min (j - i) (as.size - i) = min (j' - i) (as.size - i) := by
@@ -387,24 +390,36 @@ theorem popWhile_append {xs ys : Array α} :
   rw [List.dropWhile_append_of_pos]
   simpa
 
-@[simp] theorem takeWhile_mkArray_eq_filter (p : α → Bool) :
-    (mkArray n a).takeWhile p = (mkArray n a).filter p := by
+@[simp] theorem takeWhile_replicate_eq_filter (p : α → Bool) :
+    (replicate n a).takeWhile p = (replicate n a).filter p := by
   simp [← List.toArray_replicate]
 
-theorem takeWhile_mkArray (p : α → Bool) :
-    (mkArray n a).takeWhile p = if p a then mkArray n a else #[] := by
-  simp [takeWhile_mkArray_eq_filter, filter_mkArray]
+@[deprecated takeWhile_replicate_eq_filter (since := "2025-03-18")]
+abbrev takeWhile_mkArray_eq_filter := @takeWhile_replicate_eq_filter
 
-@[simp] theorem popWhile_mkArray_eq_filter_not (p : α → Bool) :
-    (mkArray n a).popWhile p = (mkArray n a).filter (fun a => !p a) := by
+theorem takeWhile_replicate (p : α → Bool) :
+    (replicate n a).takeWhile p = if p a then replicate n a else #[] := by
+  simp [takeWhile_replicate_eq_filter, filter_replicate]
+
+@[deprecated takeWhile_replicate (since := "2025-03-18")]
+abbrev takeWhile_mkArray := @takeWhile_replicate
+
+@[simp] theorem popWhile_replicate_eq_filter_not (p : α → Bool) :
+    (replicate n a).popWhile p = (replicate n a).filter (fun a => !p a) := by
   simp [← List.toArray_replicate, ← List.filter_reverse]
 
-theorem popWhile_mkArray (p : α → Bool) :
-    (mkArray n a).popWhile p = if p a then #[] else mkArray n a := by
-  simp only [popWhile_mkArray_eq_filter_not, size_mkArray, filter_mkArray, Bool.not_eq_eq_eq_not,
+@[deprecated popWhile_replicate_eq_filter_not (since := "2025-03-18")]
+abbrev popWhile_mkArray_eq_filter_not := @popWhile_replicate_eq_filter_not
+
+theorem popWhile_replicate (p : α → Bool) :
+    (replicate n a).popWhile p = if p a then #[] else replicate n a := by
+  simp only [popWhile_replicate_eq_filter_not, size_replicate, filter_replicate, Bool.not_eq_eq_eq_not,
     Bool.not_true]
   split <;> simp_all
 
+@[deprecated popWhile_replicate (since := "2025-03-18")]
+abbrev popWhile_mkArray := @popWhile_replicate
+
 theorem extract_takeWhile {as : Array α} {i : Nat} :
     (as.takeWhile p).extract 0 i = (as.extract 0 i).takeWhile p := by
   rcases as with ⟨as⟩

src/Init/Data/Array/Find.lean

@@ -99,21 +99,33 @@ theorem getElem_zero_flatten {xss : Array (Array α)} (h) :
   simp [getElem?_eq_getElem, h] at t
   simp [← t]
 
-theorem findSome?_mkArray : findSome? f (mkArray n a) = if n = 0 then none else f a := by
+theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
   simp [← List.toArray_replicate, List.findSome?_replicate]
 
-@[simp] theorem findSome?_mkArray_of_pos (h : 0 < n) : findSome? f (mkArray n a) = f a := by
-  simp [findSome?_mkArray, Nat.ne_of_gt h]
+@[deprecated findSome?_replicate (since := "2025-03-18")]
+abbrev findSome?_mkArray := @findSome?_replicate
+
+@[simp] theorem findSome?_replicate_of_pos (h : 0 < n) : findSome? f (replicate n a) = f a := by
+  simp [findSome?_replicate, Nat.ne_of_gt h]
+
+@[deprecated findSome?_replicate_of_pos (since := "2025-03-18")]
+abbrev findSome?_mkArray_of_pos := @findSome?_replicate_of_pos
 
 -- Argument is unused, but used to decide whether `simp` should unfold.
-@[simp] theorem findSome?_mkArray_of_isSome (_ : (f a).isSome) :
-   findSome? f (mkArray n a) = if n = 0 then none else f a := by
-  simp [findSome?_mkArray]
+@[simp] theorem findSome?_replicate_of_isSome (_ : (f a).isSome) :
+   findSome? f (replicate n a) = if n = 0 then none else f a := by
+  simp [findSome?_replicate]
 
-@[simp] theorem findSome?_mkArray_of_isNone (h : (f a).isNone) :
-    findSome? f (mkArray n a) = none := by
+@[deprecated findSome?_replicate_of_isSome (since := "2025-03-18")]
+abbrev findSome?_mkArray_of_isSome := @findSome?_replicate_of_isSome
+
+@[simp] theorem findSome?_replicate_of_isNone (h : (f a).isNone) :
+    findSome? f (replicate n a) = none := by
   rw [Option.isNone_iff_eq_none] at h
-  simp [findSome?_mkArray, h]
+  simp [findSome?_replicate, h]
+
+@[deprecated findSome?_replicate_of_isNone (since := "2025-03-18")]
+abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone
 
 /-! ### find? -/
 
@@ -254,40 +266,58 @@ theorem find?_flatMap_eq_none_iff {xs : Array α} {f : α → Array β} {p : β
 @[deprecated find?_flatMap_eq_none_iff (since := "2025-02-03")]
 abbrev find?_flatMap_eq_none := @find?_flatMap_eq_none_iff
 
-theorem find?_mkArray :
-    find? p (mkArray n a) = if n = 0 then none else if p a then some a else none := by
+theorem find?_replicate :
+    find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   simp [← List.toArray_replicate, List.find?_replicate]
 
-@[simp] theorem find?_mkArray_of_length_pos (h : 0 < n) :
-    find? p (mkArray n a) = if p a then some a else none := by
-  simp [find?_mkArray, Nat.ne_of_gt h]
+@[deprecated find?_replicate (since := "2025-03-18")]
+abbrev find?_mkArray := @find?_replicate
 
-@[simp] theorem find?_mkArray_of_pos (h : p a) :
-    find? p (mkArray n a) = if n = 0 then none else some a := by
-  simp [find?_mkArray, h]
+@[simp] theorem find?_replicate_of_size_pos (h : 0 < n) :
+    find? p (replicate n a) = if p a then some a else none := by
+  simp [find?_replicate, Nat.ne_of_gt h]
 
-@[simp] theorem find?_mkArray_of_neg (h : ¬ p a) : find? p (mkArray n a) = none := by
-  simp [find?_mkArray, h]
+@[deprecated find?_replicate_of_size_pos (since := "2025-03-18")]
+abbrev find?_mkArray_of_length_pos := @find?_replicate_of_size_pos
+
+@[simp] theorem find?_replicate_of_pos (h : p a) :
+    find? p (replicate n a) = if n = 0 then none else some a := by
+  simp [find?_replicate, h]
+
+@[deprecated find?_replicate_of_pos (since := "2025-03-18")]
+abbrev find?_mkArray_of_pos := @find?_replicate_of_pos
+
+@[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
+  simp [find?_replicate, h]
+
+@[deprecated find?_replicate_of_neg (since := "2025-03-18")]
+abbrev find?_mkArray_of_neg := @find?_replicate_of_neg
 
 -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
-theorem find?_mkArray_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
-    (mkArray n a).find? p = none ↔ n = 0 ∨ !p a := by
+theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
+    (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
   simp [← List.toArray_replicate, List.find?_replicate_eq_none_iff, Classical.or_iff_not_imp_left]
 
-@[deprecated find?_mkArray_eq_none_iff (since := "2025-02-03")]
-abbrev find?_mkArray_eq_none := @find?_mkArray_eq_none_iff
+@[deprecated find?_replicate_eq_none_iff (since := "2025-03-18")]
+abbrev find?_mkArray_eq_none_iff := @find?_replicate_eq_none_iff
 
-@[simp] theorem find?_mkArray_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
-    (mkArray n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
+@[simp] theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
+    (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
   simp [← List.toArray_replicate]
 
-@[deprecated find?_mkArray_eq_some_iff (since := "2025-02-03")]
-abbrev find?_mkArray_eq_some := @find?_mkArray_eq_some_iff
+@[deprecated find?_replicate_eq_some_iff (since := "2025-03-18")]
+abbrev find?_mkArray_eq_some_iff := @find?_replicate_eq_some_iff
 
-@[simp] theorem get_find?_mkArray (n : Nat) (a : α) (p : α → Bool) (h) :
-    ((mkArray n a).find? p).get h = a := by
+@[deprecated find?_replicate_eq_some_iff (since := "2025-02-03")]
+abbrev find?_mkArray_eq_some := @find?_replicate_eq_some_iff
+
+@[simp] theorem get_find?_replicate (n : Nat) (a : α) (p : α → Bool) (h) :
+    ((replicate n a).find? p).get h = a := by
   simp [← List.toArray_replicate]
 
+@[deprecated get_find?_replicate (since := "2025-03-18")]
+abbrev get_find?_mkArray := @get_find?_replicate
+
 theorem find?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
     (H : ∀ (a : α), a ∈ xs → P a) (p : β → Bool) :
     (xs.pmap f H).find? p = (xs.attach.find? (fun ⟨a, m⟩ => p (f a (H a m)))).map fun ⟨a, m⟩ => f a (H a m) := by
@@ -481,12 +511,15 @@ theorem findIdx?_flatten {xss : Array (Array α)} {p : α → Bool} :
   cases xss using array₂_induction
   simp [List.findIdx?_flatten, Function.comp_def]
 
-@[simp] theorem findIdx?_mkArray :
-    (mkArray n a).findIdx? p = if 0 < n ∧ p a then some 0 else none := by
+@[simp] theorem findIdx?_replicate :
+    (replicate n a).findIdx? p = if 0 < n ∧ p a then some 0 else none := by
   rw [← List.toArray_replicate]
   simp only [List.findIdx?_toArray]
   simp
 
+@[deprecated findIdx?_replicate (since := "2025-03-18")]
+abbrev findIdx?_mkArray := @findIdx?_replicate
+
 theorem findIdx?_eq_findSome?_zipIdx {xs : Array α} {p : α → Bool} :
     xs.findIdx? p = xs.zipIdx.findSome? fun ⟨a, i⟩ => if p a then some i else none := by
   rcases xs with ⟨xs⟩

src/Init/Data/Array/Lemmas.lean

@@ -321,27 +321,45 @@ theorem eq_push_of_size_ne_zero {xs : Array α} (h : xs.size ≠ 0) :
 theorem singleton_inj : #[a] = #[b] ↔ a = b := by
   simp
 
-/-! ### mkArray -/
+/-! ### replicate -/
 
-@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
+@[simp] theorem size_replicate (n : Nat) (v : α) : (replicate n v).size = n :=
   List.length_replicate ..
 
-@[simp] theorem toList_mkArray : (mkArray n a).toList = List.replicate n a := by
-  simp only [mkArray]
+@[deprecated size_replicate (since := "2025-03-18")]
+abbrev size_mkArray := @size_replicate
 
-@[simp] theorem mkArray_zero : mkArray 0 a = #[] := rfl
+@[simp] theorem toList_replicate : (replicate n a).toList = List.replicate n a := by
+  simp only [replicate]
 
-theorem mkArray_succ : mkArray (n + 1) a = (mkArray n a).push a := by
+@[deprecated toList_replicate (since := "2025-03-18")]
+abbrev toList_mkArray := @toList_replicate
+
+@[simp] theorem replicate_zero : replicate 0 a = #[] := rfl
+
+@[deprecated replicate_zero (since := "2025-03-18")]
+abbrev mkArray_zero := @replicate_zero
+
+theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by
   apply toList_inj.1
   simp [List.replicate_succ']
 
-@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
-    (mkArray n v)[i] = v := by simp [← getElem_toList]
+@[deprecated replicate_succ (since := "2025-03-18")]
+abbrev mkArray_succ := @replicate_succ
 
-theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
-    (mkArray n v)[i]? = if i < n then some v else none := by
+@[simp] theorem getElem_replicate (n : Nat) (v : α) (h : i < (replicate n v).size) :
+    (replicate n v)[i] = v := by simp [← getElem_toList]
+
+@[deprecated getElem_replicate (since := "2025-03-18")]
+abbrev getElem_mkArray := @getElem_replicate
+
+@[simp] theorem getElem?_replicate (n : Nat) (v : α) (i : Nat) :
+    (replicate n v)[i]? = if i < n then some v else none := by
   simp [getElem?_def]
 
+@[deprecated getElem?_replicate (since := "2025-03-18")]
+abbrev getElem?_mkArray := @getElem?_replicate
+
 /-! ### mem -/
 
 theorem not_mem_empty (a : α) : ¬ a ∈ #[] := by simp
@@ -1037,15 +1055,18 @@ theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys
   cases ys
   simp [List.length_eq_of_beq (by simpa using h)]
 
-@[simp] theorem mkArray_beq_mkArray [BEq α] {a b : α} {n : Nat} :
-    (mkArray n a == mkArray n b) = (n == 0 || a == b) := by
+@[simp] theorem replicate_beq_replicate [BEq α] {a b : α} {n : Nat} :
+    (replicate n a == replicate n b) = (n == 0 || a == b) := by
   cases n with
   | zero => simp
   | succ n =>
-    rw [mkArray_succ, mkArray_succ, push_beq_push, mkArray_beq_mkArray]
+    rw [replicate_succ, replicate_succ, push_beq_push, replicate_beq_replicate]
     rw [Bool.eq_iff_iff]
     simp +contextual
 
+@[deprecated replicate_beq_replicate (since := "2025-03-18")]
+abbrev mkArray_beq_mkArray := @replicate_beq_replicate
+
 private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a == b := by
   intro h
   have : isEqv #[a] #[b] BEq.beq = true := h
@@ -2306,147 +2327,234 @@ theorem flatMap_eq_foldl (f : α → Array β) (xs : Array α) :
     rw [List.foldl_cons, ih]
     simp [toArray_append]
 
-/-! ### mkArray -/
+/-! ### replicate -/
 
-@[simp] theorem mkArray_one : mkArray 1 a = #[a] := rfl
+@[simp] theorem replicate_one : replicate 1 a = #[a] := rfl
 
-/-- Variant of `mkArray_succ` that prepends `a` at the beginning of the array. -/
-theorem mkArray_succ' : mkArray (n + 1) a = #[a] ++ mkArray n a := by
+@[deprecated replicate_one (since := "2025-03-18")]
+abbrev mkArray_one := @replicate_one
+
+/-- Variant of `replicate_succ` that prepends `a` at the beginning of the array. -/
+theorem replicate_succ' : replicate (n + 1) a = #[a] ++ replicate n a := by
   apply Array.ext'
   simp [List.replicate_succ]
 
-@[simp] theorem mem_mkArray {a b : α} {n} : b ∈ mkArray n a ↔ n ≠ 0 ∧ b = a := by
-  unfold mkArray
+@[deprecated replicate_succ' (since := "2025-03-18")]
+abbrev mkArray_succ' := @replicate_succ'
+
+@[simp] theorem mem_replicate {a b : α} {n} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by
+  unfold replicate
   simp only [mem_toArray, List.mem_replicate]
 
-theorem eq_of_mem_mkArray {a b : α} {n} (h : b ∈ mkArray n a) : b = a := (mem_mkArray.1 h).2
+@[deprecated mem_replicate (since := "2025-03-18")]
+abbrev mem_mkArray := @mem_replicate
 
-theorem forall_mem_mkArray {p : α → Prop} {a : α} {n} :
-    (∀ b, b ∈ mkArray n a → p b) ↔ n = 0 ∨ p a := by
-  cases n <;> simp [mem_mkArray]
+theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a := (mem_replicate.1 h).2
 
-@[simp] theorem mkArray_succ_ne_empty (n : Nat) (a : α) : mkArray (n+1) a ≠ #[] := by
-  simp [mkArray_succ]
+@[deprecated eq_of_mem_mkArray (since := "2025-03-18")]
+abbrev eq_of_mem_mkArray := @eq_of_mem_replicate
 
-@[simp] theorem mkArray_eq_empty_iff {n : Nat} (a : α) : mkArray n a = #[] ↔ n = 0 := by
+theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
+    (∀ b, b ∈ replicate n a → p b) ↔ n = 0 ∨ p a := by
+  cases n <;> simp [mem_replicate]
+
+@[deprecated forall_mem_replicate (since := "2025-03-18")]
+abbrev forall_mem_mkArray := @forall_mem_replicate
+
+@[simp] theorem replicate_succ_ne_empty (n : Nat) (a : α) : replicate (n+1) a ≠ #[] := by
+  simp [replicate_succ]
+
+@[deprecated replicate_succ_ne_empty (since := "2025-03-18")]
+abbrev mkArray_succ_ne_empty := @replicate_succ_ne_empty
+
+@[simp] theorem replicate_eq_empty_iff {n : Nat} (a : α) : replicate n a = #[] ↔ n = 0 := by
   cases n <;> simp
 
-@[simp] theorem getElem?_mkArray_of_lt {n : Nat} {i : Nat} (h : i < n) : (mkArray n a)[i]? = some a := by
-  simp [getElem?_mkArray, h]
+@[deprecated replicate_eq_empty_iff (since := "2025-03-18")]
+abbrev mkArray_eq_empty_iff := @replicate_eq_empty_iff
 
-@[simp] theorem mkArray_inj : mkArray n a = mkArray m b ↔ n = m ∧ (n = 0 ∨ a = b) := by
+@[simp] theorem replicate_inj : replicate n a = replicate m b ↔ n = m ∧ (n = 0 ∨ a = b) := by
   rw [← toList_inj]
   simp
 
-theorem eq_mkArray_of_mem {a : α} {xs : Array α} (h : ∀ (b) (_ : b ∈ xs), b = a) : xs = mkArray xs.size a := by
+@[deprecated replicate_inj (since := "2025-03-18")]
+abbrev mkArray_inj := @replicate_inj
+
+theorem eq_replicate_of_mem {a : α} {xs : Array α} (h : ∀ (b) (_ : b ∈ xs), b = a) : xs = replicate xs.size a := by
   rw [← toList_inj]
   simpa using List.eq_replicate_of_mem (by simpa using h)
 
-theorem eq_mkArray_iff {a : α} {n} {xs : Array α} :
-    xs = mkArray n a ↔ xs.size = n ∧ ∀ (b) (_ : b ∈ xs), b = a := by
+@[deprecated eq_replicate_of_mem (since := "2025-03-18")]
+abbrev eq_mkArray_of_mem := @eq_replicate_of_mem
+
+theorem eq_replicate_iff {a : α} {n} {xs : Array α} :
+    xs = replicate n a ↔ xs.size = n ∧ ∀ (b) (_ : b ∈ xs), b = a := by
   rw [← toList_inj]
   simpa using List.eq_replicate_iff (l := xs.toList)
 
-theorem map_eq_mkArray_iff {xs : Array α} {f : α → β} {b : β} :
-    xs.map f = mkArray xs.size b ↔ ∀ x ∈ xs, f x = b := by
-  simp [eq_mkArray_iff]
+@[deprecated eq_replicate_iff (since := "2025-03-18")]
+abbrev eq_mkArray_iff := @eq_replicate_iff
 
-@[simp] theorem map_const (xs : Array α) (b : β) : map (Function.const α b) xs = mkArray xs.size b :=
-  map_eq_mkArray_iff.mpr fun _ _ => rfl
+theorem map_eq_replicate_iff {xs : Array α} {f : α → β} {b : β} :
+    xs.map f = replicate xs.size b ↔ ∀ x ∈ xs, f x = b := by
+  simp [eq_replicate_iff]
 
-@[simp] theorem map_const_fun (x : β) : map (Function.const α x) = (mkArray ·.size x) := by
+@[deprecated map_eq_replicate_iff (since := "2025-03-18")]
+abbrev map_eq_mkArray_iff := @map_eq_replicate_iff
+
+@[simp] theorem map_const (xs : Array α) (b : β) : map (Function.const α b) xs = replicate xs.size b :=
+  map_eq_replicate_iff.mpr fun _ _ => rfl
+
+@[simp] theorem map_const_fun (x : β) : map (Function.const α x) = (replicate ·.size x) := by
   funext xs
   simp
 
 /-- Variant of `map_const` using a lambda rather than `Function.const`. -/
 -- This can not be a `@[simp]` lemma because it would fire on every `List.map`.
-theorem map_const' (xs : Array α) (b : β) : map (fun _ => b) xs = mkArray xs.size b :=
+theorem map_const' (xs : Array α) (b : β) : map (fun _ => b) xs = replicate xs.size b :=
   map_const xs b
 
-@[simp] theorem set_mkArray_self : (mkArray n a).set i a h = mkArray n a := by
+@[simp] theorem set_replicate_self : (replicate n a).set i a h = replicate n a := by
   apply Array.ext'
   simp
 
-@[simp] theorem setIfInBounds_mkArray_self : (mkArray n a).setIfInBounds i a = mkArray n a := by
+@[deprecated set_replicate_self (since := "2025-03-18")]
+abbrev set_mkArray_self := @set_replicate_self
+
+@[simp] theorem setIfInBounds_replicate_self : (replicate n a).setIfInBounds i a = replicate n a := by
   apply Array.ext'
   simp
 
-@[simp] theorem mkArray_append_mkArray : mkArray n a ++ mkArray m a = mkArray (n + m) a := by
+@[deprecated setIfInBounds_replicate_self (since := "2025-03-18")]
+abbrev setIfInBounds_mkArray_self := @setIfInBounds_replicate_self
+
+@[simp] theorem replicate_append_replicate : replicate n a ++ replicate m a = replicate (n + m) a := by
   apply Array.ext'
   simp
 
-theorem append_eq_mkArray_iff {xs ys : Array α} {a : α} :
-    xs ++ ys = mkArray n a ↔
-      xs.size + ys.size = n ∧ xs = mkArray xs.size a ∧ ys = mkArray ys.size a := by
+@[deprecated replicate_append_replicate (since := "2025-03-18")]
+abbrev mkArray_append_mkArray := @replicate_append_replicate
+
+theorem append_eq_replicate_iff {xs ys : Array α} {a : α} :
+    xs ++ ys = replicate n a ↔
+      xs.size + ys.size = n ∧ xs = replicate xs.size a ∧ ys = replicate ys.size a := by
   simp [← toList_inj, List.append_eq_replicate_iff]
 
-theorem mkArray_eq_append_iff {xs ys : Array α} {a : α} :
-    mkArray n a = xs ++ ys ↔
-      xs.size + ys.size = n ∧ xs = mkArray xs.size a ∧ ys = mkArray ys.size a := by
-  rw [eq_comm, append_eq_mkArray_iff]
+@[deprecated append_eq_replicate_iff (since := "2025-03-18")]
+abbrev append_eq_mkArray_iff := @append_eq_replicate_iff
 
-@[simp] theorem map_mkArray : (mkArray n a).map f = mkArray n (f a) := by
+theorem replicate_eq_append_iff {xs ys : Array α} {a : α} :
+    replicate n a = xs ++ ys ↔
+      xs.size + ys.size = n ∧ xs = replicate xs.size a ∧ ys = replicate ys.size a := by
+  rw [eq_comm, append_eq_replicate_iff]
+
+@[deprecated replicate_eq_append_iff (since := "2025-03-18")]
+abbrev replicate_eq_mkArray_iff := @replicate_eq_append_iff
+
+@[simp] theorem map_replicate : (replicate n a).map f = replicate n (f a) := by
   apply Array.ext'
   simp
 
-theorem filter_mkArray (w : stop = n) :
-    (mkArray n a).filter p 0 stop = if p a then mkArray n a else #[] := by
+@[deprecated map_replicate (since := "2025-03-18")]
+abbrev map_mkArray := @map_replicate
+
+theorem filter_replicate (w : stop = n) :
+    (replicate n a).filter p 0 stop = if p a then replicate n a else #[] := by
   apply Array.ext'
-  simp only [w, toList_filter', toList_mkArray, List.filter_replicate]
+  simp only [w, toList_filter', toList_replicate, List.filter_replicate]
   split <;> simp_all
 
-@[simp] theorem filter_mkArray_of_pos (w : stop = n) (h : p a) :
-    (mkArray n a).filter p 0 stop = mkArray n a := by
-  simp [filter_mkArray, h, w]
+@[deprecated filter_replicate (since := "2025-03-18")]
+abbrev filter_mkArray := @filter_replicate
 
-@[simp] theorem filter_mkArray_of_neg (w : stop = n) (h : ¬ p a) :
-    (mkArray n a).filter p 0 stop = #[] := by
-  simp [filter_mkArray, h, w]
+@[simp] theorem filter_replicate_of_pos (w : stop = n) (h : p a) :
+    (replicate n a).filter p 0 stop = replicate n a := by
+  simp [filter_replicate, h, w]
 
-theorem filterMap_mkArray {f : α → Option β} (w : stop = n := by simp) :
-    (mkArray n a).filterMap f 0 stop = match f a with | none => #[] | .some b => mkArray n b := by
+@[deprecated filter_replicate_of_pos (since := "2025-03-18")]
+abbrev filter_mkArray_of_pos := @filter_replicate_of_pos
+
+@[simp] theorem filter_replicate_of_neg (w : stop = n) (h : ¬ p a) :
+    (replicate n a).filter p 0 stop = #[] := by
+  simp [filter_replicate, h, w]
+
+@[deprecated filter_replicate_of_neg (since := "2025-03-18")]
+abbrev filter_mkArray_of_neg := @filter_replicate_of_neg
+
+theorem filterMap_replicate {f : α → Option β} (w : stop = n := by simp) :
+    (replicate n a).filterMap f 0 stop = match f a with | none => #[] | .some b => replicate n b := by
   apply Array.ext'
-  simp only [w, size_mkArray, toList_filterMap', toList_mkArray, List.filterMap_replicate]
+  simp only [w, size_replicate, toList_filterMap', toList_replicate, List.filterMap_replicate]
   split <;> simp_all
 
+@[deprecated filterMap_replicate (since := "2025-03-18")]
+abbrev filterMap_mkArray := @filterMap_replicate
+
 -- This is not a useful `simp` lemma because `b` is unknown.
-theorem filterMap_mkArray_of_some {f : α → Option β} (h : f a = some b) :
-    (mkArray n a).filterMap f = mkArray n b := by
-  simp [filterMap_mkArray, h]
+theorem filterMap_replicate_of_some {f : α → Option β} (h : f a = some b) :
+    (replicate n a).filterMap f = replicate n b := by
+  simp [filterMap_replicate, h]
 
-@[simp] theorem filterMap_mkArray_of_isSome {f : α → Option β} (h : (f a).isSome) :
-    (mkArray n a).filterMap f = mkArray n (Option.get _ h) := by
+@[deprecated filterMap_replicate_of_some (since := "2025-03-18")]
+abbrev filterMap_mkArray_of_some := @filterMap_replicate_of_some
+
+@[simp] theorem filterMap_replicate_of_isSome {f : α → Option β} (h : (f a).isSome) :
+    (replicate n a).filterMap f = replicate n (Option.get _ h) := by
   match w : f a, h with
-  | some b, _ => simp [filterMap_mkArray, h, w]
+  | some b, _ => simp [filterMap_replicate, h, w]
 
-@[simp] theorem filterMap_mkArray_of_none {f : α → Option β} (h : f a = none) :
-    (mkArray n a).filterMap f = #[] := by
-  simp [filterMap_mkArray, h]
+@[deprecated filterMap_replicate_of_isSome (since := "2025-03-18")]
+abbrev filterMap_mkArray_of_isSome := @filterMap_replicate_of_isSome
 
-@[simp] theorem flatten_mkArray_empty : (mkArray n (#[] : Array α)).flatten = #[] := by
+@[simp] theorem filterMap_replicate_of_none {f : α → Option β} (h : f a = none) :
+    (replicate n a).filterMap f = #[] := by
+  simp [filterMap_replicate, h]
+
+@[deprecated filterMap_replicate_of_none (since := "2025-03-18")]
+abbrev filterMap_mkArray_of_none := @filterMap_replicate_of_none
+
+@[simp] theorem flatten_replicate_empty : (replicate n (#[] : Array α)).flatten = #[] := by
   rw [← toList_inj]
   simp
 
-@[simp] theorem flatten_mkArray_singleton : (mkArray n #[a]).flatten = mkArray n a := by
+@[deprecated flatten_replicate_empty (since := "2025-03-18")]
+abbrev flatten_mkArray_empty := @flatten_replicate_empty
+
+@[simp] theorem flatten_replicate_singleton : (replicate n #[a]).flatten = replicate n a := by
   rw [← toList_inj]
   simp
 
-@[simp] theorem flatten_mkArray_mkArray : (mkArray n (mkArray m a)).flatten = mkArray (n * m) a := by
+@[deprecated flatten_replicate_singleton (since := "2025-03-18")]
+abbrev flatten_mkArray_singleton := @flatten_replicate_singleton
+
+@[simp] theorem flatten_replicate_replicate : (replicate n (replicate m a)).flatten = replicate (n * m) a := by
   rw [← toList_inj]
   simp
 
-theorem flatMap_mkArray {β} (f : α → Array β) : (mkArray n a).flatMap f = (mkArray n (f a)).flatten := by
+@[deprecated flatten_replicate_replicate (since := "2025-03-18")]
+abbrev flatten_mkArray_replicate := @flatten_replicate_replicate
+
+theorem flatMap_replicate {β} (f : α → Array β) : (replicate n a).flatMap f = (replicate n (f a)).flatten := by
   rw [← toList_inj]
   simp [flatMap_toList, List.flatMap_replicate]
 
-@[simp] theorem isEmpty_mkArray : (mkArray n a).isEmpty = decide (n = 0) := by
+@[deprecated flatMap_replicate (since := "2025-03-18")]
+abbrev flatMap_mkArray := @flatMap_replicate
+
+@[simp] theorem isEmpty_replicate : (replicate n a).isEmpty = decide (n = 0) := by
   rw [← List.toArray_replicate, List.isEmpty_toArray]
   simp
 
-@[simp] theorem sum_mkArray_nat (n : Nat) (a : Nat) : (mkArray n a).sum = n * a := by
+@[deprecated isEmpty_replicate (since := "2025-03-18")]
+abbrev isEmpty_mkArray := @isEmpty_replicate
+
+@[simp] theorem sum_replicate_nat (n : Nat) (a : Nat) : (replicate n a).sum = n * a := by
   rw [← List.toArray_replicate, List.sum_toArray]
   simp
 
+@[deprecated sum_replicate_nat (since := "2025-03-18")]
+abbrev sum_mkArray_nat := @sum_replicate_nat
+
 /-! ### Preliminaries about `swap` needed for `reverse`. -/
 
 theorem getElem?_swap (xs : Array α) (i j : Nat) (hi hj) (k : Nat) : (xs.swap i j hi hj)[k]? =
@@ -2625,10 +2733,13 @@ theorem flatMap_reverse {β} (xs : Array α) (f : α → Array β) :
   cases xs
   simp [List.flatMap_reverse, Function.comp_def]
 
-@[simp] theorem reverse_mkArray (n) (a : α) : reverse (mkArray n a) = mkArray n a := by
+@[simp] theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a := by
   rw [← toList_inj]
   simp
 
+@[deprecated reverse_replicate (since := "2025-03-18")]
+abbrev reverse_mkArray := @reverse_replicate
+
 /-! ### extract -/
 
 theorem extract_loop_zero (xs ys : Array α) (start : Nat) : extract.loop xs 0 start ys = ys := by
@@ -3464,14 +3575,20 @@ theorem back?_flatten {xss : Array (Array α)} :
     (flatten xss).back? = xss.reverse.findSome? fun xs => xs.back? := by
   simp [← flatMap_id, back?_flatMap]
 
-theorem back?_mkArray (a : α) (n : Nat) :
-    (mkArray n a).back? = if n = 0 then none else some a := by
-  rw [mkArray_eq_toArray_replicate]
+theorem back?_replicate (a : α) (n : Nat) :
+    (replicate n a).back? = if n = 0 then none else some a := by
+  rw [replicate_eq_toArray_replicate]
   simp only [List.back?_toArray, List.getLast?_replicate]
 
-@[simp] theorem back_mkArray (w : 0 < n) : (mkArray n a).back (by simpa using w) = a := by
+@[deprecated back?_replicate (since := "2025-03-18")]
+abbrev back?_mkArray := @back?_replicate
+
+@[simp] theorem back_replicate (w : 0 < n) : (replicate n a).back (by simpa using w) = a := by
   simp [back_eq_getElem]
 
+@[deprecated back_replicate (since := "2025-03-18")]
+abbrev back_mkArray := @back_replicate
+
 /-! ## Additional operations -/
 
 /-! ### leftpad -/
@@ -3508,9 +3625,12 @@ theorem pop_append {xs ys : Array α} :
     (xs ++ ys).pop = if ys.isEmpty then xs.pop else xs ++ ys.pop := by
   split <;> simp_all
 
-@[simp] theorem pop_mkArray (n) (a : α) : (mkArray n a).pop = mkArray (n - 1) a := by
+@[simp] theorem pop_replicate (n) (a : α) : (replicate n a).pop = replicate (n - 1) a := by
   ext <;> simp
 
+@[deprecated pop_replicate (since := "2025-03-18")]
+abbrev pop_mkArray := @pop_replicate
+
 /-! ### modify -/
 
 @[simp] theorem size_modify (xs : Array α) (i : Nat) (f : α → α) : (xs.modify i f).size = xs.size := by
@@ -3675,15 +3795,21 @@ theorem replace_extract {xs : Array α} {i : Nat} :
   rcases xs with ⟨xs⟩
   simp [List.replace_take]
 
-@[simp] theorem replace_mkArray_self {a : α} (h : 0 < n) :
-    (mkArray n a).replace a b = #[b] ++ mkArray (n - 1) a := by
-  cases n <;> simp_all [mkArray_succ', replace_append]
+@[simp] theorem replace_replicate_self {a : α} (h : 0 < n) :
+    (replicate n a).replace a b = #[b] ++ replicate (n - 1) a := by
+  cases n <;> simp_all [replicate_succ', replace_append]
 
-@[simp] theorem replace_mkArray_ne {a b c : α} (h : !b == a) :
-    (mkArray n a).replace b c = mkArray n a := by
+@[deprecated replace_replicate_self (since := "2025-03-18")]
+abbrev replace_mkArray_self := @replace_replicate_self
+
+@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
+    (replicate n a).replace b c = replicate n a := by
   rw [replace_of_not_mem]
   simp_all
 
+@[deprecated replace_replicate_ne (since := "2025-03-18")]
+abbrev replace_mkArray_ne := @replace_replicate_ne
+
 end replace
 
 /-! ## Logic -/
@@ -3911,13 +4037,19 @@ theorem any_reverse {xs : Array α} : xs.reverse.any f 0 = xs.any f := by
 theorem all_reverse {xs : Array α} : xs.reverse.all f 0 = xs.all f := by
   simp
 
-@[simp] theorem any_mkArray {n : Nat} {a : α} :
-    (mkArray n a).any f = if n = 0 then false else f a := by
-  induction n <;> simp_all [mkArray_succ']
+@[simp] theorem any_replicate {n : Nat} {a : α} :
+    (replicate n a).any f = if n = 0 then false else f a := by
+  induction n <;> simp_all [replicate_succ']
 
-@[simp] theorem all_mkArray {n : Nat} {a : α} :
-    (mkArray n a).all f = if n = 0 then true else f a := by
-  induction n <;> simp_all +contextual [mkArray_succ']
+@[deprecated any_replicate (since := "2025-03-18")]
+abbrev any_mkArray := @any_replicate
+
+@[simp] theorem all_replicate {n : Nat} {a : α} :
+    (replicate n a).all f = if n = 0 then true else f a := by
+  induction n <;> simp_all +contextual [replicate_succ']
+
+@[deprecated all_replicate (since := "2025-03-18")]
+abbrev all_mkArray := @all_replicate
 
 /-! ### toListRev -/
 

src/Init/Data/Array/MapIdx.lean

@@ -292,12 +292,15 @@ theorem mapFinIdx_eq_mapFinIdx_iff {xs : Array α} {f g : (i : Nat) → α → (
     (xs.mapFinIdx f).mapFinIdx g = xs.mapFinIdx (fun i a h => g i (f i a h) (by simpa using h)) := by
   simp [mapFinIdx_eq_iff]
 
-theorem mapFinIdx_eq_mkArray_iff {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} {b : β} :
-    xs.mapFinIdx f = mkArray xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] h = b := by
+theorem mapFinIdx_eq_replicate_iff {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} {b : β} :
+    xs.mapFinIdx f = replicate xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] h = b := by
   rcases xs with ⟨l⟩
   rw [← toList_inj]
   simp [List.mapFinIdx_eq_replicate_iff]
 
+@[deprecated mapFinIdx_eq_replicate_iff (since := "2025-03-18")]
+abbrev mapFinIdx_eq_mkArray_iff := @mapFinIdx_eq_replicate_iff
+
 @[simp] theorem mapFinIdx_reverse {xs : Array α} {f : (i : Nat) → α → (h : i < xs.reverse.size) → β} :
     xs.reverse.mapFinIdx f = (xs.mapFinIdx (fun i a h => f (xs.size - 1 - i) a (by simp; omega))).reverse := by
   rcases xs with ⟨l⟩
@@ -431,12 +434,15 @@ theorem mapIdx_eq_mapIdx_iff {xs : Array α} :
     (xs.mapIdx f).mapIdx g = xs.mapIdx (fun i => g i ∘ f i) := by
   simp [mapIdx_eq_iff]
 
-theorem mapIdx_eq_mkArray_iff {xs : Array α} {f : Nat → α → β} {b : β} :
-    mapIdx f xs = mkArray xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] = b := by
+theorem mapIdx_eq_replicate_iff {xs : Array α} {f : Nat → α → β} {b : β} :
+    mapIdx f xs = replicate xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] = b := by
   rcases xs with ⟨xs⟩
   rw [← toList_inj]
   simp [List.mapIdx_eq_replicate_iff]
 
+@[deprecated mapIdx_eq_replicate_iff (since := "2025-03-18")]
+abbrev mapIdx_eq_mkArray_iff := @mapIdx_eq_replicate_iff
+
 @[simp] theorem mapIdx_reverse {xs : Array α} {f : Nat → α → β} :
     xs.reverse.mapIdx f = (mapIdx (fun i => f (xs.size - 1 - i)) xs).reverse := by
   rcases xs with ⟨xs⟩

src/Init/Data/Array/Subarray.lean

@@ -7,6 +7,7 @@ prelude
 import Init.Data.Array.Basic
 
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.missingDocs true
 
 universe u v w
 
@@ -25,7 +26,18 @@ structure Subarray (α : Type u) where
   start : Nat
   /-- The ending index of the region of interest (exclusive). -/
   stop : Nat
+  /--
+  The starting index is no later than the ending index.
+
+  The ending index is exclusive. If the starting and ending indices are equal, then the subarray is
+  empty.
+  -/
   start_le_stop : start ≤ stop
+  /-- The stopping index is no later than the end of the array.
+
+  The ending index is exclusive. If it is equal to the size of the array, then the last element of
+  the array is in the subarray.
+  -/
   stop_le_array_size : stop ≤ array.size
 
 namespace Subarray
@@ -110,6 +122,12 @@ instance : EmptyCollection (Subarray α) :=
 instance : Inhabited (Subarray α) :=
   ⟨{}⟩
 
+/--
+The run-time implementation of `ForIn.forIn` for `Subarray`, which allows it to be used with `for`
+loops in `do`-notation.
+
+This definition replaces `Subarray.forIn`.
+-/
 @[inline] unsafe def forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β :=
   let sz := USize.ofNat s.stop
   let rec @[specialize] loop (i : USize) (b : β) : m β := do
@@ -122,6 +140,10 @@ instance : Inhabited (Subarray α) :=
       pure b
   loop (USize.ofNat s.start) b
 
+/--
+The implementation of `ForIn.forIn` for `Subarray`, which allows it to be used with `for` loops in
+`do`-notation.
+-/
 -- TODO: provide reference implementation
 @[implemented_by Subarray.forInUnsafe]
 protected opaque forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β :=

src/Init/Data/Array/Zip.lean

@@ -149,10 +149,13 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {as : Array α} {bs : Array
   · rintro ⟨⟨ws⟩, ⟨xs⟩, ⟨ys⟩, ⟨zs⟩, h, rfl, rfl, h₁, h₂⟩
     exact ⟨ws, xs, ys, zs, by simp_all⟩
 
-@[simp] theorem zipWith_mkArray {a : α} {b : β} {m n : Nat} :
-    zipWith f (mkArray m a) (mkArray n b) = mkArray (min m n) (f a b) := by
+@[simp] theorem zipWith_replicate {a : α} {b : β} {m n : Nat} :
+    zipWith f (replicate m a) (replicate n b) = replicate (min m n) (f a b) := by
   simp [← List.toArray_replicate]
 
+@[deprecated zipWith_replicate (since := "2025-03-18")]
+abbrev zipWith_mkArray := @zipWith_replicate
+
 theorem map_uncurry_zip_eq_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
     map (Function.uncurry f) (as.zip bs) = zipWith f as bs := by
   cases as
@@ -270,10 +273,13 @@ theorem zip_eq_append_iff {as : Array α} {bs : Array β} :
       ∃ as₁ as₂ bs₁ bs₂, as₁.size = bs₁.size ∧ as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = zip as₁ bs₁ ∧ ys = zip as₂ bs₂ := by
   simp [zip_eq_zipWith, zipWith_eq_append_iff]
 
-@[simp] theorem zip_mkArray {a : α} {b : β} {m n : Nat} :
-    zip (mkArray m a) (mkArray n b) = mkArray (min m n) (a, b) := by
+@[simp] theorem zip_replicate {a : α} {b : β} {m n : Nat} :
+    zip (replicate m a) (replicate n b) = replicate (min m n) (a, b) := by
   simp [← List.toArray_replicate]
 
+@[deprecated zip_replicate (since := "2025-03-18")]
+abbrev zip_mkArray := @zip_replicate
+
 theorem zip_eq_zip_take_min (as : Array α) (bs : Array β) :
     zip as bs = zip (as.take (min as.size bs.size)) (bs.take (min as.size bs.size)) := by
   cases as
@@ -317,9 +323,12 @@ theorem map_zipWithAll {δ : Type _} (f : α → β) (g : Option γ → Option
   simp [List.map_zipWithAll]
 
 @[simp] theorem zipWithAll_replicate {a : α} {b : β} {n : Nat} :
-    zipWithAll f (mkArray n a) (mkArray n b) = mkArray n (f a b) := by
+    zipWithAll f (replicate n a) (replicate n b) = replicate n (f a b) := by
   simp [← List.toArray_replicate]
 
+@[deprecated zipWithAll_replicate (since := "2025-03-18")]
+abbrev zipWithAll_mkArray := @zipWithAll_replicate
+
 /-! ### unzip -/
 
 @[simp] theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by
@@ -360,6 +369,9 @@ theorem zip_of_prod {as : Array α} {bs : Array β} {xs : Array (α × β)} (hl
     (hr : xs.map Prod.snd = bs) : xs = as.zip bs := by
   rw [← hl, ← hr, ← zip_unzip xs, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
 
-@[simp] theorem unzip_mkArray {n : Nat} {a : α} {b : β} :
-    unzip (mkArray n (a, b)) = (mkArray n a, mkArray n b) := by
+@[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
+    unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
   ext1 <;> simp
+
+@[deprecated unzip_replicate (since := "2025-03-18")]
+abbrev unzip_mkArray := @unzip_replicate

src/Init/Data/BitVec/Bitblast.lean

@@ -1350,4 +1350,53 @@ theorem eq_iff_eq_of_inv (f : α → BitVec w) (g : BitVec w → α) (h : ∀ x,
     have := congrArg g h'
     simpa [h] using this
 
+/-! ### Lemmas that use Bitblasting circuits -/
+
+theorem add_sub_comm {x y : BitVec w} : x + y - z = x - z + y := by
+  apply eq_of_toNat_eq
+  simp only [toNat_sub, toNat_add, add_mod_mod, mod_add_mod]
+  congr 1
+  omega
+
+theorem sub_add_comm {x y : BitVec w} : x - y + z = x + z - y := by
+  rw [add_sub_comm]
+
+theorem not_add_one {x : BitVec w} : ~~~ (x + 1#w) = ~~~ x - 1#w := by
+  rw [not_eq_neg_add, not_eq_neg_add, neg_add]
+
+theorem not_add_eq_not_neg {x y : BitVec w} : ~~~ (x + y) = ~~~ x - y := by
+  rw [not_eq_neg_add, not_eq_neg_add, neg_add]
+  simp only [sub_toAdd]
+  rw [BitVec.add_assoc, @BitVec.add_comm _ (-y), ← BitVec.add_assoc]
+
+theorem not_sub_one_eq_not_add_one {x : BitVec w} : ~~~ (x - 1#w) = ~~~ x + 1#w := by
+  rw [not_eq_neg_add, not_eq_neg_add, neg_sub,
+    BitVec.add_sub_cancel, BitVec.sub_add_cancel]
+
+theorem not_sub_eq_not_add {x y : BitVec w} : ~~~ (x - y) = ~~~ x + y := by
+  rw [BitVec.sub_toAdd, not_add_eq_not_neg, sub_neg]
+
+/-- The value of `(carry i x y false)` can be computed by truncating `x` and `y`
+to `len` bits where `len ≥ i`. -/
+theorem carry_extractLsb'_eq_carry {w i len : Nat} (hi : i < len)
+    {x y : BitVec w} {b : Bool}: 
+    (carry i (extractLsb' 0 len x) (extractLsb' 0 len y) b)
+    = (carry i x y b) := by
+  simp only [carry, extractLsb'_toNat, shiftRight_zero, toNat_false, Nat.add_zero, ge_iff_le,
+    decide_eq_decide]
+  have : 2 ^ i ∣ 2^len := by
+    apply Nat.pow_dvd_pow
+    omega
+  rw [Nat.mod_mod_of_dvd _ this, Nat.mod_mod_of_dvd _ this]
+
+/--
+The `[0..len)` low bits of `x + y` can be computed by truncating `x` and `y`
+to `len` bits and then adding.
+-/
+theorem extractLsb'_add {w len : Nat} {x y : BitVec w} (hlen : len ≤ w) : 
+    (x + y).extractLsb' 0 len = x.extractLsb' 0 len + y.extractLsb' 0 len := by
+  ext i hi
+  rw [getElem_extractLsb', Nat.zero_add, getLsbD_add (by omega)]
+  simp [getElem_add, carry_extractLsb'_eq_carry hi, getElem_extractLsb', Nat.zero_add]
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -1081,6 +1081,17 @@ theorem getElem_eq_extractLsb' (x : BitVec w) (i : Nat) (h : i < w) :
     x[i] = (x.extractLsb' i 1 == 1#1) := by
   rw [← getLsbD_eq_getElem, getLsbD_eq_extractLsb']
 
+@[simp]
+theorem extractLsb'_zero {w start len : Nat} : (0#w).extractLsb' start len = 0#len := by
+  apply eq_of_toNat_eq
+  simp [extractLsb']
+
+@[simp]
+theorem extractLsb'_eq_zero {x : BitVec w} {start : Nat} :
+    x.extractLsb' start 0 = 0#0 := by
+  ext i hi
+  omega
+
 /-! ### allOnes -/
 
 @[simp] theorem toNat_allOnes : (allOnes v).toNat = 2^v - 1 := by
@@ -1562,6 +1573,22 @@ theorem not_self_ne {a : BitVec w} (h : 0 < w) : ~~~a ≠ a := by
   rw [ne_comm]
   simp [h]
 
+theorem not_and {x y : BitVec w} : ~~~ (x &&& y) = ~~~ x ||| ~~~ y := by
+  ext i
+  simp
+
+theorem not_or {x y : BitVec w} : ~~~ (x ||| y) = ~~~ x &&& ~~~ y := by
+  ext i
+  simp
+
+theorem not_xor_left {x y : BitVec w} : ~~~ (x ^^^ y) = ~~~ x ^^^ y := by
+  ext i
+  simp
+
+theorem not_xor_right {x y : BitVec w} : ~~~ (x ^^^ y) = x ^^^ ~~~ y := by
+  ext i
+  simp
+
 /-! ### cast -/
 
 @[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(x.cast h) = (~~~x).cast h := by

src/Init/Data/Float.lean

@@ -140,15 +140,27 @@ instance : ToString Float where
 @[extern "lean_uint16_to_float"] opaque UInt16.toFloat (n : UInt16) : Float
 /-- Obtains the `Float` whose value is the same as the given `UInt32`. -/
 @[extern "lean_uint32_to_float"] opaque UInt32.toFloat (n : UInt32) : Float
-/-- Obtains a `Float` whose value is near the given `UInt64`. It will be exactly the value of the
-given `UInt64` if such a `Float` exists. If no such `Float` exists, the returned value will either
-be the smallest `Float` this is larger than the given value, or the largest `Float` this is smaller
-than the given value. -/
+/--
+Obtains a `Float` whose value is near the given `UInt64`.
+
+It will be exactly the value of the given `UInt64` if such a `Float` exists. If no such `Float`
+exists, the returned value will either be the smallest `Float` that is larger than the given value,
+or the largest `Float` that is smaller than the given value.
+
+This function is opaque in the kernel, but is overridden at runtime with an efficient
+implementation.
+-/
 @[extern "lean_uint64_to_float"] opaque UInt64.toFloat (n : UInt64) : Float
-/-- Obtains a `Float` whose value is near the given `USize`. It will be exactly the value of the
-given `USize` if such a `Float` exists. If no such `Float` exists, the returned value will either
-be the smallest `Float` this is larger than the given value, or the largest `Float` this is smaller
-than the given value. -/
+/--
+Obtains a `Float` whose value is near the given `USize`.
+
+It will be exactly the value of the given `USize` if such a `Float` exists. If no such `Float`
+exists, the returned value will either be the smallest `Float` that is larger than the given value,
+or the largest `Float` that is smaller than the given value.
+
+This function is opaque in the kernel, but is overridden at runtime with an efficient
+implementation.
+-/
 @[extern "lean_usize_to_float"] opaque USize.toFloat (n : USize) : Float
 
 instance : Inhabited Float where

src/Init/Data/Float32.lean

@@ -131,20 +131,37 @@ instance : ToString Float32 where
 @[extern "lean_uint8_to_float32"] opaque UInt8.toFloat32 (n : UInt8) : Float32
 /-- Obtains the `Float32` whose value is the same as the given `UInt16`. -/
 @[extern "lean_uint16_to_float32"] opaque UInt16.toFloat32 (n : UInt16) : Float32
-/-- Obtains a `Float32` whose value is near the given `UInt32`. It will be exactly the value of the
-given `UInt32` if such a `Float32` exists. If no such `Float32` exists, the returned value will either
-be the smallest `Float32` this is larger than the given value, or the largest `Float32` this is smaller
-than the given value. -/
+/--
+Obtains a `Float32` whose value is near the given `UInt32`.
+
+It will be exactly the value of the given `UInt32` if such a `Float32` exists. If no such `Float32`
+exists, the returned value will either be the smallest `Float32` that is larger than the given
+value, or the largest `Float32` that is smaller than the given value.
+
+This function is opaque in the kernel, but is overridden at runtime with an efficient
+implementation.
+-/
 @[extern "lean_uint32_to_float32"] opaque UInt32.toFloat32 (n : UInt32) : Float32
-/-- Obtains a `Float32` whose value is near the given `UInt64`. It will be exactly the value of the
-given `UInt64` if such a `Float32` exists. If no such `Float32` exists, the returned value will either
-be the smallest `Float32` this is larger than the given value, or the largest `Float32` this is smaller
-than the given value. -/
+/--
+Obtains a `Float32` whose value is near the given `UInt64`.
+
+It will be exactly the value of the given `UInt64` if such a `Float32` exists. If no such `Float32`
+exists, the returned value will either be the smallest `Float32` that is larger than the given
+value, or the largest `Float32` that is smaller than the given value.
+
+This function is opaque in the kernel, but is overridden at runtime with an efficient
+implementation.
+-/
 @[extern "lean_uint64_to_float32"] opaque UInt64.toFloat32 (n : UInt64) : Float32
-/-- Obtains a `Float32` whose value is near the given `USize`. It will be exactly the value of the
-given `USize` if such a `Float32` exists. If no such `Float32` exists, the returned value will either
-be the smallest `Float32` this is larger than the given value, or the largest `Float32` this is smaller
-than the given value. -/
+/-- Obtains a `Float32` whose value is near the given `USize`.
+
+It will be exactly the value of the given `USize` if such a `Float32` exists. If no such `Float32`
+exists, the returned value will either be the smallest `Float32` that is larger than the given
+value, or the largest `Float32` that is smaller than the given value.
+
+This function is opaque in the kernel, but is overridden at runtime with an efficient
+implementation.
+-/
 @[extern "lean_usize_to_float32"] opaque USize.toFloat32 (n : USize) : Float32
 
 instance : Inhabited Float32 where

src/Init/Data/List/ToArray.lean

@@ -538,11 +538,16 @@ private theorem popWhile_toArray_aux (p : α → Bool) (l : List α) :
   · simp
   · simp_all [List.set_eq_of_length_le]
 
-@[simp] theorem toArray_replicate (n : Nat) (v : α) : (List.replicate n v).toArray = mkArray n v := rfl
+@[simp] theorem toArray_replicate (n : Nat) (v : α) :
+    (List.replicate n v).toArray = Array.replicate n v := rfl
 
-theorem _root_.Array.mkArray_eq_toArray_replicate : mkArray n v = (List.replicate n v).toArray := by
+theorem _root_.Array.replicate_eq_toArray_replicate :
+    Array.replicate n v = (List.replicate n v).toArray := by
   simp
 
+@[deprecated _root_.Array.replicate_eq_toArray_replicate (since := "2025-03-18")]
+abbrev _root_.Array.mkArray_eq_toArray_replicate := @_root_.Array.replicate_eq_toArray_replicate
+
 @[simp] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl
 
 theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) :

src/Init/Data/Nat/Div/Basic.lean

@@ -39,7 +39,7 @@ Examples:
  * `0 / 22 = 0`
  * `5 / 0 = 0`
 -/
-@[extern "lean_nat_div"]
+@[extern "lean_nat_div", irreducible]
 protected def div (x y : @& Nat) : Nat :=
   if hy : 0 < y then
     let rec
@@ -140,7 +140,7 @@ reductions](lean-manual://section/type-system) when the `Nat`s contain free vari
 This function is overridden at runtime with an efficient implementation. This definition is the
 logical model.
 -/
-@[extern "lean_nat_mod"]
+@[extern "lean_nat_mod", irreducible]
 protected noncomputable def modCore (x y : Nat) : Nat :=
   if hy : 0 < y then
     let rec

src/Init/Data/OfScientific.lean

@@ -17,6 +17,16 @@ import Init.Data.Nat.Log2
    Note the use of `nat_lit`; there is no wrapping `OfNat.ofNat` in the resulting term.
 -/
 class OfScientific (α : Type u) where
+  /--
+  Produces a value from the given mantissa, exponent sign, and decimal exponent. For the exponent
+  sign, `true` indicates a negative exponent.
+
+   Examples:
+   - `1.23` is syntax for `OfScientific.ofScientific (nat_lit 123) true (nat_lit 2)`
+   - `121e100` is syntax for `OfScientific.ofScientific (nat_lit 121) false (nat_lit 100)`
+
+   Note the use of `nat_lit`; there is no wrapping `OfNat.ofNat` in the resulting term.
+  -/
   ofScientific (mantissa : Nat) (exponentSign : Bool) (decimalExponent : Nat) : α
 
 /-- Computes `m * 2^e`. -/

src/Init/Data/Random.lean

@@ -34,11 +34,15 @@ structure StdGen where
 
 instance : Inhabited StdGen := ⟨{ s1 := 0, s2 := 0 }⟩
 
+/-- The range of values returned by `StdGen` -/
 def stdRange := (1, 2147483562)
 
 instance : Repr StdGen where
   reprPrec | ⟨s1, s2⟩, _ => Std.Format.bracket "⟨" (repr s1 ++ ", " ++ repr s2) "⟩"
 
+/--
+The next value from a `StdGen`, paired with an updated generator state.
+-/
 def stdNext : StdGen → Nat × StdGen
   | ⟨s1, s2⟩ =>
     let k    : Int := Int.ofNat (s1 / 53668)
@@ -51,6 +55,9 @@ def stdNext : StdGen → Nat × StdGen
     let z'   : Nat := if z < 1 then (z + 2147483562).toNat else z.toNat % 2147483562
     (z', ⟨s1'', s2''⟩)
 
+/--
+Splits a `StdGen` into two separate states.
+-/
 def stdSplit : StdGen → StdGen × StdGen
   | g@⟨s1, s2⟩ =>
     let newS1  := if s1 = 2147483562 then 1 else s1 + 1

src/Init/Data/Repr.lean

@@ -180,6 +180,16 @@ Examples:
 def toDigits (base : Nat) (n : Nat) : List Char :=
   toDigitsCore base (n+1) n []
 
+/--
+Converts a word-sized unsigned integer into a decimal string.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `USize.repr 0 = "0"`
+ * `USize.repr 28 = "28"`
+ * `USize.repr 307 = "307"`
+-/
 @[extern "lean_string_of_usize"]
 protected def _root_.USize.repr (n : @& USize) : String :=
   (toDigits 10 n.toNat).asString

src/Init/Data/SInt/Float.lean

@@ -7,6 +7,8 @@ prelude
 import Init.Data.Float
 import Init.Data.SInt.Basic
 
+set_option linter.missingDocs true
+
 /--
 Truncates the value to the nearest integer, rounding towards zero.
 If NaN, returns `0`.
@@ -59,13 +61,25 @@ If smaller than the minimum value for `ISize` (including -Inf), returns the mini
 @[extern "lean_int16_to_float"] opaque Int16.toFloat (n : Int16) : Float
 /-- Obtains the `Float` whose value is the same as the given `Int32`. -/
 @[extern "lean_int32_to_float"] opaque Int32.toFloat (n : Int32) : Float
-/-- Obtains a `Float` whose value is near the given `Int64`. It will be exactly the value of the
-given `Int64` if such a `Float` exists. If no such `Float` exists, the returned value will either
-be the smallest `Float` this is larger than the given value, or the largest `Float` this is smaller
-than the given value. -/
+/--
+Obtains a `Float` whose value is near the given `Int64`.
+
+It will be exactly the value of the given `Int64` if such a `Float` exists. If no such `Float`
+exists, the returned value will either be the smallest `Float` that is larger than the given value,
+or the largest `Float` that is smaller than the given value.
+
+This function is opaque in the kernel, but is overridden at runtime with an efficient
+implementation.
+-/
 @[extern "lean_int64_to_float"] opaque Int64.toFloat (n : Int64) : Float
-/-- Obtains a `Float` whose value is near the given `ISize`. It will be exactly the value of the
-given `ISize` if such a `Float` exists. If no such `Float` exists, the returned value will either
-be the smallest `Float` this is larger than the given value, or the largest `Float` this is smaller
-than the given value. -/
+/--
+Obtains a `Float` whose value is near the given `ISize`.
+
+It will be exactly the value of the given `ISize` if such a `Float` exists. If no such `Float`
+exists, the returned value will either be the smallest `Float` that is larger than the given value,
+or the largest `Float` that is smaller than the given value.
+
+This function is opaque in the kernel, but is overridden at runtime with an efficient
+implementation.
+-/
 @[extern "lean_isize_to_float"] opaque ISize.toFloat (n : ISize) : Float

src/Init/Data/SInt/Float32.lean

@@ -7,6 +7,8 @@ prelude
 import Init.Data.Float32
 import Init.Data.SInt.Basic
 
+set_option linter.missingDocs true
+
 /--
 Truncates the value to the nearest integer, rounding towards zero.
 If NaN, returns `0`.
@@ -57,18 +59,27 @@ If smaller than the minimum value for `ISize` (including -Inf), returns the mini
 @[extern "lean_int8_to_float32"] opaque Int8.toFloat32 (n : Int8) : Float32
 /-- Obtains the `Float32` whose value is the same as the given `Int16`. -/
 @[extern "lean_int16_to_float32"] opaque Int16.toFloat32 (n : Int16) : Float32
-/-- Obtains a `Float32` whose value is near the given `Int32`. It will be exactly the value of the
-given `Int32` if such a `Float32` exists. If no such `Float32` exists, the returned value will either
-be the smallest `Float32` this is larger than the given value, or the largest `Float32` this is smaller
-than the given value. -/
+/--
+Obtains a `Float32` whose value is near the given `Int32`.
+
+It will be exactly the value of the given `Int32` if such a `Float32` exists. If no such `Float32`
+exists, the returned value will either be the smallest `Float32` that is larger than the given
+value, or the largest `Float32` that is smaller than the given value.
+-/
 @[extern "lean_int32_to_float32"] opaque Int32.toFloat32 (n : Int32) : Float32
-/-- Obtains a `Float32` whose value is near the given `Int64`. It will be exactly the value of the
-given `Int64` if such a `Float32` exists. If no such `Float32` exists, the returned value will either
-be the smallest `Float32` this is larger than the given value, or the largest `Float32` this is smaller
-than the given value. -/
+/--
+Obtains a `Float32` whose value is near the given `Int64`.
+
+It will be exactly the value of the given `Int64` if such a `Float32` exists. If no such `Float32`
+exists, the returned value will either be the smallest `Float32` that is larger than the given
+value, or the largest `Float32` that is smaller than the given value.
+-/
 @[extern "lean_int64_to_float32"] opaque Int64.toFloat32 (n : Int64) : Float32
-/-- Obtains a `Float32` whose value is near the given `ISize`. It will be exactly the value of the
-given `ISize` if such a `Float32` exists. If no such `Float32` exists, the returned value will either
-be the smallest `Float32` this is larger than the given value, or the largest `Float32` this is smaller
-than the given value. -/
+/--
+Obtains a `Float32` whose value is near the given `ISize`.
+
+It will be exactly the value of the given `ISize` if such a `Float32` exists. If no such `Float32`
+exists, the returned value will either be the smallest `Float32` that is larger than the given
+value, or the largest `Float32` that is smaller than the given value.
+-/
 @[extern "lean_isize_to_float32"] opaque ISize.toFloat32 (n : ISize) : Float32

src/Init/Data/String/Basic.lean

@@ -1414,9 +1414,29 @@ end Substring
 
 namespace String
 
+/--
+Removes the specified number of characters (Unicode code points) from the start of the string.
+
+If `n` is greater than `s.length`, returns `""`.
+
+Examples:
+ * `"red green blue".drop 4 = "green blue"`
+ * `"red green blue".drop 10 = "blue"`
+ * `"red green blue".drop 50 = ""`
+-/
 @[inline] def drop (s : String) (n : Nat) : String :=
   (s.toSubstring.drop n).toString
 
+/--
+Removes the specified number of characters (Unicode code points) from the end of the string.
+
+If `n` is greater than `s.length`, returns `""`.
+
+Examples:
+ * `"red green blue".dropRight 5 = "red green"`
+ * `"red green blue".dropRight 11 = "red"`
+ * `"red green blue".dropRight 50 = ""`
+-/
 @[inline] def dropRight (s : String) (n : Nat) : String :=
   (s.toSubstring.dropRight n).toString
 

src/Init/Data/UInt/Basic.lean

@@ -7,6 +7,8 @@ prelude
 import Init.Data.UInt.BasicAux
 import Init.Data.BitVec.Basic
 
+set_option linter.missingDocs true
+
 open Nat
 
 /-- Converts a `Fin UInt8.size` into the corresponding `UInt8`. -/
@@ -18,29 +20,110 @@ def UInt8.mk (bitVec : BitVec 8) : UInt8 :=
 def UInt8.ofNatCore (n : Nat) (h : n < UInt8.size) : UInt8 :=
   UInt8.ofNatLT n h
 
+/--
+Adds two 8-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
+operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_add"]
 def UInt8.add (a b : UInt8) : UInt8 := ⟨a.toBitVec + b.toBitVec⟩
+/--
+Subtracts one 8-bit unsigned integer from another, wrapping around on underflow. Usually accessed
+via the `-` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_sub"]
 def UInt8.sub (a b : UInt8) : UInt8 := ⟨a.toBitVec - b.toBitVec⟩
+/--
+Multiplies two 8-bit unsigned integers, wrapping around on overflow.  Usually accessed via the `*`
+operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_mul"]
 def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.toBitVec * b.toBitVec⟩
+/--
+Unsigned division for 8-bit unsigned integers, discarding the remainder. Usually accessed
+via the `/` operator.
+
+This operation is sometimes called “floor division.” Division by zero is defined to be zero.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_div"]
 def UInt8.div (a b : UInt8) : UInt8 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
+/--
+The modulo operator for 8-bit unsigned integers, which computes the remainder when dividing one
+integer by another. Usually accessed via the `%` operator.
+
+When the divisor is `0`, the result is the dividend rather than an error.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+* `UInt8.mod 5 2 = 1`
+* `UInt8.mod 4 2 = 0`
+* `UInt8.mod 4 0 = 4`
+-/
 @[extern "lean_uint8_mod"]
 def UInt8.mod (a b : UInt8) : UInt8 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+set_option linter.missingDocs false in
 @[deprecated UInt8.mod (since := "2024-09-23")]
 def UInt8.modn (a : UInt8) (n : Nat) : UInt8 := ⟨Fin.modn a.toFin n⟩
+/--
+Bitwise and for 8-bit unsigned integers. Usually accessed via the `&&&` operator.
+
+Each bit of the resulting integer is set if the corresponding bits of both input integers are set.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_land"]
 def UInt8.land (a b : UInt8) : UInt8 := ⟨a.toBitVec &&& b.toBitVec⟩
+/--
+Bitwise or for 8-bit unsigned integers. Usually accessed via the `|||` operator.
+
+Each bit of the resulting integer is set if at least one of the corresponding bits of both input
+integers are set.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_lor"]
 def UInt8.lor (a b : UInt8) : UInt8 := ⟨a.toBitVec ||| b.toBitVec⟩
+/--
+Bitwise exclusive or for 8-bit unsigned integers. Usually accessed via the `^^^` operator.
+
+Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
+integers are set.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_xor"]
 def UInt8.xor (a b : UInt8) : UInt8 := ⟨a.toBitVec ^^^ b.toBitVec⟩
+/--
+Bitwise left shift for 8-bit unsigned integers. Usually accessed via the `<<<` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_shift_left"]
 def UInt8.shiftLeft (a b : UInt8) : UInt8 := ⟨a.toBitVec <<< (mod b 8).toBitVec⟩
+/--
+Bitwise right shift for 8-bit unsigned integers. Usually accessed via the `>>>` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_shift_right"]
 def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.toBitVec >>> (mod b 8).toBitVec⟩
+/--
+Strict inequality of 8-bit unsigned integers, defined as inequality of the corresponding
+natural numbers. Usually accessed via the `<` operator.
+-/
 def UInt8.lt (a b : UInt8) : Prop := a.toBitVec < b.toBitVec
+/--
+Non-strict inequality of 8-bit unsigned integers, defined as inequality of the corresponding
+natural numbers. Usually accessed via the `≤` operator.
+-/
 def UInt8.le (a b : UInt8) : Prop := a.toBitVec ≤ b.toBitVec
 
 instance : Add UInt8       := ⟨UInt8.add⟩
@@ -55,8 +138,23 @@ instance : Div UInt8       := ⟨UInt8.div⟩
 instance : LT UInt8        := ⟨UInt8.lt⟩
 instance : LE UInt8        := ⟨UInt8.le⟩
 
+/--
+Bitwise complement, also known as bitwise negation, for 8-bit unsigned integers. Usually accessed
+via the `~~~` prefix operator.
+
+Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_complement"]
 def UInt8.complement (a : UInt8) : UInt8 := ⟨~~~a.toBitVec⟩
+/--
+Negation of 8-bit unsigned integers, computed modulo `UInt8.size`.
+
+`UInt8.neg a` is equivalent to `255 - a + 1`.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_neg"]
 def UInt8.neg (a : UInt8) : UInt8 := ⟨-a.toBitVec⟩
 
@@ -74,10 +172,33 @@ Converts `true` to `1` and `false` to `0`.
 @[extern "lean_bool_to_uint8"]
 def Bool.toUInt8 (b : Bool) : UInt8 := if b then 1 else 0
 
+/--
+Decides whether one 8-bit unsigned integer is strictly less than another. Usually accessed via the
+`DecidableLT UInt8` instance.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `(if (6 : UInt8) < 7 then "yes" else "no") = "yes"`
+ * `(if (5 : UInt8) < 5 then "yes" else "no") = "no"`
+ * `show ¬((7 : UInt8) < 7) by decide`
+-/
 @[extern "lean_uint8_dec_lt"]
 def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
+/--
+Decides whether one 8-bit unsigned integer is less than or equal to another. Usually accessed via the
+`DecidableLE UInt8` instance.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `(if (15 : UInt8) ≤ 15 then "yes" else "no") = "yes"`
+ * `(if (15 : UInt8) ≤ 5 then "yes" else "no") = "no"`
+ * `(if (5 : UInt8) ≤ 15 then "yes" else "no") = "yes"`
+ * `show (7 : UInt8) ≤ 7 by decide`
+-/
 @[extern "lean_uint8_dec_le"]
 def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
@@ -96,29 +217,110 @@ def UInt16.mk (bitVec : BitVec 16) : UInt16 :=
 def UInt16.ofNatCore (n : Nat) (h : n < UInt16.size) : UInt16 :=
   UInt16.ofNatLT n h
 
+/--
+Adds two 16-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
+operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_add"]
 def UInt16.add (a b : UInt16) : UInt16 := ⟨a.toBitVec + b.toBitVec⟩
+/--
+Subtracts one 16-bit unsigned integer from another, wrapping around on underflow. Usually accessed
+via the `-` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_sub"]
 def UInt16.sub (a b : UInt16) : UInt16 := ⟨a.toBitVec - b.toBitVec⟩
+/--
+Multiplies two 16-bit unsigned integers, wrapping around on overflow.  Usually accessed via the `*`
+operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_mul"]
 def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.toBitVec * b.toBitVec⟩
+/--
+Unsigned division for 16-bit unsigned integers, discarding the remainder. Usually accessed
+via the `/` operator.
+
+This operation is sometimes called “floor division.” Division by zero is defined to be zero.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_div"]
 def UInt16.div (a b : UInt16) : UInt16 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
+/--
+The modulo operator for 16-bit unsigned integers, which computes the remainder when dividing one
+integer by another. Usually accessed via the `%` operator.
+
+When the divisor is `0`, the result is the dividend rather than an error.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+* `UInt16.mod 5 2 = 1`
+* `UInt16.mod 4 2 = 0`
+* `UInt16.mod 4 0 = 4`
+-/
 @[extern "lean_uint16_mod"]
 def UInt16.mod (a b : UInt16) : UInt16 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+set_option linter.missingDocs false in
 @[deprecated UInt16.mod (since := "2024-09-23")]
 def UInt16.modn (a : UInt16) (n : Nat) : UInt16 := ⟨Fin.modn a.toFin n⟩
+/--
+Bitwise and for 16-bit unsigned integers. Usually accessed via the `&&&` operator.
+
+Each bit of the resulting integer is set if the corresponding bits of both input integers are set.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_land"]
 def UInt16.land (a b : UInt16) : UInt16 := ⟨a.toBitVec &&& b.toBitVec⟩
+/--
+Bitwise or for 16-bit unsigned integers. Usually accessed via the `|||` operator.
+
+Each bit of the resulting integer is set if at least one of the corresponding bits of both input
+integers are set.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_lor"]
 def UInt16.lor (a b : UInt16) : UInt16 := ⟨a.toBitVec ||| b.toBitVec⟩
+/--
+Bitwise exclusive or for 8-bit unsigned integers. Usually accessed via the `^^^` operator.
+
+Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
+integers are set.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_xor"]
 def UInt16.xor (a b : UInt16) : UInt16 := ⟨a.toBitVec ^^^ b.toBitVec⟩
+/--
+Bitwise left shift for 16-bit unsigned integers. Usually accessed via the `<<<` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_shift_left"]
 def UInt16.shiftLeft (a b : UInt16) : UInt16 := ⟨a.toBitVec <<< (mod b 16).toBitVec⟩
+/--
+Bitwise right shift for 16-bit unsigned integers. Usually accessed via the `>>>` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_shift_right"]
 def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.toBitVec >>> (mod b 16).toBitVec⟩
+/--
+Strict inequality of 16-bit unsigned integers, defined as inequality of the corresponding
+natural numbers. Usually accessed via the `<` operator.
+-/
 def UInt16.lt (a b : UInt16) : Prop := a.toBitVec < b.toBitVec
+/--
+Non-strict inequality of 16-bit unsigned integers, defined as inequality of the corresponding
+natural numbers. Usually accessed via the `≤` operator.
+-/
 def UInt16.le (a b : UInt16) : Prop := a.toBitVec ≤ b.toBitVec
 
 instance : Add UInt16       := ⟨UInt16.add⟩
@@ -133,8 +335,23 @@ instance : Div UInt16       := ⟨UInt16.div⟩
 instance : LT UInt16        := ⟨UInt16.lt⟩
 instance : LE UInt16        := ⟨UInt16.le⟩
 
+/--
+Bitwise complement, also known as bitwise negation, for 16-bit unsigned integers. Usually accessed
+via the `~~~` prefix operator.
+
+Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_complement"]
 def UInt16.complement (a : UInt16) : UInt16 := ⟨~~~a.toBitVec⟩
+/--
+Negation of 16-bit unsigned integers, computed modulo `UInt16.size`.
+
+`UInt16.neg a` is equivalent to `65_535 - a + 1`.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_neg"]
 def UInt16.neg (a : UInt16) : UInt16 := ⟨-a.toBitVec⟩
 
@@ -153,11 +370,34 @@ Converts `true` to `1` and `false` to `0`.
 def Bool.toUInt16 (b : Bool) : UInt16 := if b then 1 else 0
 
 set_option bootstrap.genMatcherCode false in
+/--
+Decides whether one 16-bit unsigned integer is strictly less than another. Usually accessed via the
+`DecidableLT UInt16` instance.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `(if (6 : UInt16) < 7 then "yes" else "no") = "yes"`
+ * `(if (5 : UInt16) < 5 then "yes" else "no") = "no"`
+ * `show ¬((7 : UInt16) < 7) by decide`
+-/
 @[extern "lean_uint16_dec_lt"]
 def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
 set_option bootstrap.genMatcherCode false in
+/--
+Decides whether one 16-bit unsigned integer is less than or equal to another. Usually accessed via the
+`DecidableLE UInt16` instance.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `(if (15 : UInt16) ≤ 15 then "yes" else "no") = "yes"`
+ * `(if (15 : UInt16) ≤ 5 then "yes" else "no") = "no"`
+ * `(if (5 : UInt16) ≤ 15 then "yes" else "no") = "yes"`
+ * `show (7 : UInt16) ≤ 7 by decide`
+-/
 @[extern "lean_uint16_dec_le"]
 def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
@@ -176,29 +416,110 @@ def UInt32.mk (bitVec : BitVec 32) : UInt32 :=
 def UInt32.ofNatCore (n : Nat) (h : n < UInt32.size) : UInt32 :=
   UInt32.ofNatLT n h
 
+/--
+Adds two 32-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
+operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint32_add"]
 def UInt32.add (a b : UInt32) : UInt32 := ⟨a.toBitVec + b.toBitVec⟩
+/--
+Subtracts one 32-bit unsigned integer from another, wrapping around on underflow. Usually accessed
+via the `-` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint32_sub"]
 def UInt32.sub (a b : UInt32) : UInt32 := ⟨a.toBitVec - b.toBitVec⟩
+/--
+Multiplies two 32-bit unsigned integers, wrapping around on overflow.  Usually accessed via the `*`
+operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint32_mul"]
 def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.toBitVec * b.toBitVec⟩
+/--
+Unsigned division for 32-bit unsigned integers, discarding the remainder. Usually accessed
+via the `/` operator.
+
+This operation is sometimes called “floor division.” Division by zero is defined to be zero.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint32_div"]
 def UInt32.div (a b : UInt32) : UInt32 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
+/--
+The modulo operator for 32-bit unsigned integers, which computes the remainder when dividing one
+integer by another. Usually accessed via the `%` operator.
+
+When the divisor is `0`, the result is the dividend rather than an error.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+* `UInt32.mod 5 2 = 1`
+* `UInt32.mod 4 2 = 0`
+* `UInt32.mod 4 0 = 4`
+-/
 @[extern "lean_uint32_mod"]
 def UInt32.mod (a b : UInt32) : UInt32 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+set_option linter.missingDocs false in
 @[deprecated UInt32.mod (since := "2024-09-23")]
 def UInt32.modn (a : UInt32) (n : Nat) : UInt32 := ⟨Fin.modn a.toFin n⟩
+/--
+Bitwise and for 32-bit unsigned integers. Usually accessed via the `&&&` operator.
+
+Each bit of the resulting integer is set if the corresponding bits of both input integers are set.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint32_land"]
 def UInt32.land (a b : UInt32) : UInt32 := ⟨a.toBitVec &&& b.toBitVec⟩
+/--
+Bitwise or for 32-bit unsigned integers. Usually accessed via the `|||` operator.
+
+Each bit of the resulting integer is set if at least one of the corresponding bits of both input
+integers are set.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint32_lor"]
 def UInt32.lor (a b : UInt32) : UInt32 := ⟨a.toBitVec ||| b.toBitVec⟩
+/--
+Bitwise exclusive or for 32-bit unsigned integers. Usually accessed via the `^^^` operator.
+
+Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
+integers are set.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint32_xor"]
 def UInt32.xor (a b : UInt32) : UInt32 := ⟨a.toBitVec ^^^ b.toBitVec⟩
+/--
+Bitwise left shift for 32-bit unsigned integers. Usually accessed via the `<<<` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint32_shift_left"]
 def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.toBitVec <<< (mod b 32).toBitVec⟩
+/--
+Bitwise right shift for 32-bit unsigned integers. Usually accessed via the `>>>` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint32_shift_right"]
 def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (mod b 32).toBitVec⟩
+/--
+Strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
+natural numbers. Usually accessed via the `<` operator.
+-/
 def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec
+/--
+Non-strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
+natural numbers. Usually accessed via the `≤` operator.
+-/
 def UInt32.le (a b : UInt32) : Prop := a.toBitVec ≤ b.toBitVec
 
 instance : Add UInt32       := ⟨UInt32.add⟩
@@ -213,8 +534,23 @@ instance : Div UInt32       := ⟨UInt32.div⟩
 instance : LT UInt32        := ⟨UInt32.lt⟩
 instance : LE UInt32        := ⟨UInt32.le⟩
 
+/--
+Bitwise complement, also known as bitwise negation, for 32-bit unsigned integers. Usually accessed
+via the `~~~` prefix operator.
+
+Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint32_complement"]
 def UInt32.complement (a : UInt32) : UInt32 := ⟨~~~a.toBitVec⟩
+/--
+Negation of 32-bit unsigned integers, computed modulo `UInt32.size`.
+
+`UInt32.neg a` is equivalent to `429_4967_295 - a + 1`.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint32_neg"]
 def UInt32.neg (a : UInt32) : UInt32 := ⟨-a.toBitVec⟩
 
@@ -241,29 +577,110 @@ def UInt64.mk (bitVec : BitVec 64) : UInt64 :=
 def UInt64.ofNatCore (n : Nat) (h : n < UInt64.size) : UInt64 :=
   UInt64.ofNatLT n h
 
+/--
+Adds two 64-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
+operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_add"]
 def UInt64.add (a b : UInt64) : UInt64 := ⟨a.toBitVec + b.toBitVec⟩
+/--
+Subtracts one 64-bit unsigned integer from another, wrapping around on underflow. Usually accessed
+via the `-` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_sub"]
 def UInt64.sub (a b : UInt64) : UInt64 := ⟨a.toBitVec - b.toBitVec⟩
+/--
+Multiplies two 64-bit unsigned integers, wrapping around on overflow.  Usually accessed via the `*`
+operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_mul"]
 def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.toBitVec * b.toBitVec⟩
+/--
+Unsigned division for 64-bit unsigned integers, discarding the remainder. Usually accessed
+via the `/` operator.
+
+This operation is sometimes called “floor division.” Division by zero is defined to be zero.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_div"]
 def UInt64.div (a b : UInt64) : UInt64 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
+/--
+The modulo operator for 64-bit unsigned integers, which computes the remainder when dividing one
+integer by another. Usually accessed via the `%` operator.
+
+When the divisor is `0`, the result is the dividend rather than an error.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+* `UInt64.mod 5 2 = 1`
+* `UInt64.mod 4 2 = 0`
+* `UInt64.mod 4 0 = 4`
+-/
 @[extern "lean_uint64_mod"]
 def UInt64.mod (a b : UInt64) : UInt64 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+set_option linter.missingDocs false in
 @[deprecated UInt64.mod (since := "2024-09-23")]
 def UInt64.modn (a : UInt64) (n : Nat) : UInt64 := ⟨Fin.modn a.toFin n⟩
+/--
+Bitwise and for 64-bit unsigned integers. Usually accessed via the `&&&` operator.
+
+Each bit of the resulting integer is set if the corresponding bits of both input integers are set.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_land"]
 def UInt64.land (a b : UInt64) : UInt64 := ⟨a.toBitVec &&& b.toBitVec⟩
+/--
+Bitwise or for 64-bit unsigned integers. Usually accessed via the `|||` operator.
+
+Each bit of the resulting integer is set if at least one of the corresponding bits of both input
+integers are set.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_lor"]
 def UInt64.lor (a b : UInt64) : UInt64 := ⟨a.toBitVec ||| b.toBitVec⟩
+/--
+Bitwise exclusive or for 64-bit unsigned integers. Usually accessed via the `^^^` operator.
+
+Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
+integers are set.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_xor"]
 def UInt64.xor (a b : UInt64) : UInt64 := ⟨a.toBitVec ^^^ b.toBitVec⟩
+/--
+Bitwise left shift for 64-bit unsigned integers. Usually accessed via the `<<<` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_shift_left"]
 def UInt64.shiftLeft (a b : UInt64) : UInt64 := ⟨a.toBitVec <<< (mod b 64).toBitVec⟩
+/--
+Bitwise right shift for 64-bit unsigned integers. Usually accessed via the `>>>` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_shift_right"]
 def UInt64.shiftRight (a b : UInt64) : UInt64 := ⟨a.toBitVec >>> (mod b 64).toBitVec⟩
+/--
+Strict inequality of 64-bit unsigned integers, defined as inequality of the corresponding
+natural numbers. Usually accessed via the `<` operator.
+-/
 def UInt64.lt (a b : UInt64) : Prop := a.toBitVec < b.toBitVec
+/--
+Non-strict inequality of 64-bit unsigned integers, defined as inequality of the corresponding
+natural numbers. Usually accessed via the `≤` operator.
+-/
 def UInt64.le (a b : UInt64) : Prop := a.toBitVec ≤ b.toBitVec
 
 instance : Add UInt64       := ⟨UInt64.add⟩
@@ -278,8 +695,23 @@ instance : Div UInt64       := ⟨UInt64.div⟩
 instance : LT UInt64        := ⟨UInt64.lt⟩
 instance : LE UInt64        := ⟨UInt64.le⟩
 
+/--
+Bitwise complement, also known as bitwise negation, for 64-bit unsigned integers. Usually accessed
+via the `~~~` prefix operator.
+
+Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_complement"]
 def UInt64.complement (a : UInt64) : UInt64 := ⟨~~~a.toBitVec⟩
+/--
+Negation of 32-bit unsigned integers, computed modulo `UInt64.size`.
+
+`UInt64.neg a` is equivalent to `18_446_744_073_709_551_615 - a + 1`.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_neg"]
 def UInt64.neg (a : UInt64) : UInt64 := ⟨-a.toBitVec⟩
 
@@ -297,10 +729,33 @@ Converts `true` to `1` and `false` to `0`.
 @[extern "lean_bool_to_uint64"]
 def Bool.toUInt64 (b : Bool) : UInt64 := if b then 1 else 0
 
+/--
+Decides whether one 64-bit unsigned integer is strictly less than another. Usually accessed via the
+`DecidableLT UInt64` instance.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `(if (6 : UInt64) < 7 then "yes" else "no") = "yes"`
+ * `(if (5 : UInt64) < 5 then "yes" else "no") = "no"`
+ * `show ¬((7 : UInt64) < 7) by decide`
+-/
 @[extern "lean_uint64_dec_lt"]
 def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
+/--
+Decides whether one 64-bit unsigned integer is less than or equal to another. Usually accessed via the
+`DecidableLE UInt64` instance.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `(if (15 : UInt64) ≤ 15 then "yes" else "no") = "yes"`
+ * `(if (15 : UInt64) ≤ 5 then "yes" else "no") = "no"`
+ * `(if (5 : UInt64) ≤ 15 then "yes" else "no") = "yes"`
+ * `show (7 : UInt64) ≤ 7 by decide`
+-/
 @[extern "lean_uint64_dec_le"]
 def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
@@ -330,53 +785,152 @@ theorem usize_size_le : USize.size ≤ 18446744073709551616 :=
 theorem le_usize_size : 4294967296 ≤ USize.size :=
   USize.le_size
 
+/--
+Multiplies two word-sized unsigned integers, wrapping around on overflow.  Usually accessed via the
+`*` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_mul"]
 def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
+/--
+Unsigned division for word-sized unsigned integers, discarding the remainder. Usually accessed
+via the `/` operator.
+
+This operation is sometimes called “floor division.” Division by zero is defined to be zero.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_div"]
 def USize.div (a b : USize) : USize := ⟨a.toBitVec / b.toBitVec⟩
+/--
+The modulo operator for word-sized unsigned integers, which computes the remainder when dividing one
+integer by another. Usually accessed via the `%` operator.
+
+When the divisor is `0`, the result is the dividend rather than an error.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+* `USize.mod 5 2 = 1`
+* `USize.mod 4 2 = 0`
+* `USize.mod 4 0 = 4`
+-/
 @[extern "lean_usize_mod"]
 def USize.mod (a b : USize) : USize := ⟨a.toBitVec % b.toBitVec⟩
+set_option linter.missingDocs false in
 @[deprecated USize.mod (since := "2024-09-23")]
 def USize.modn (a : USize) (n : Nat) : USize := ⟨Fin.modn a.toFin n⟩
+/--
+Bitwise and for word-sized unsigned integers. Usually accessed via the `&&&` operator.
+
+Each bit of the resulting integer is set if the corresponding bits of both input integers are set.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_land"]
 def USize.land (a b : USize) : USize := ⟨a.toBitVec &&& b.toBitVec⟩
+/--
+Bitwise or for word-sized unsigned integers. Usually accessed via the `|||` operator.
+
+Each bit of the resulting integer is set if at least one of the corresponding bits of both input
+integers are set.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_lor"]
 def USize.lor (a b : USize) : USize := ⟨a.toBitVec ||| b.toBitVec⟩
+/--
+Bitwise exclusive or for word-sized unsigned integers. Usually accessed via the `^^^` operator.
+
+Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
+integers are set.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_xor"]
 def USize.xor (a b : USize) : USize := ⟨a.toBitVec ^^^ b.toBitVec⟩
+/--
+Bitwise left shift for word-sized unsigned integers. Usually accessed via the `<<<` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_shift_left"]
 def USize.shiftLeft (a b : USize) : USize := ⟨a.toBitVec <<< (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
+/--
+Bitwise right shift for word-sized unsigned integers. Usually accessed via the `>>>` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_shift_right"]
 def USize.shiftRight (a b : USize) : USize := ⟨a.toBitVec >>> (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
 /--
-Upcast a `Nat` less than `2^32` to a `USize`.
-This is lossless because `USize.size` is either `2^32` or `2^64`.
-This function is overridden with a native implementation.
+Converts a natural number to a `USize`. Overflow is impossible on any supported platform because
+`USize.size` is either `2^32` or `2^64`.
+
+This function is overridden at runtime with an efficient implementation.
 -/
 @[extern "lean_usize_of_nat"]
 def USize.ofNat32 (n : @& Nat) (h : n < 4294967296) : USize :=
   USize.ofNatLT n (Nat.lt_of_lt_of_le h USize.le_size)
+/--
+Converts 8-bit unsigned integers to word-sized unsigned integers.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_to_usize"]
 def UInt8.toUSize (a : UInt8) : USize :=
   USize.ofNat32 a.toBitVec.toNat (Nat.lt_trans a.toBitVec.isLt (by decide))
+/--
+Converts word-sized unsigned integers to 8-bit unsigned integers. Wraps around on overflow.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_to_uint8"]
 def USize.toUInt8 (a : USize) : UInt8 := a.toNat.toUInt8
+/--
+Converts 16-bit unsigned integers to word-sized unsigned integers.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_to_usize"]
 def UInt16.toUSize (a : UInt16) : USize :=
   USize.ofNat32 a.toBitVec.toNat (Nat.lt_trans a.toBitVec.isLt (by decide))
+/--
+Converts word-sized unsigned integers to 16-bit unsigned integers. Wraps around on overflow.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_to_uint16"]
 def USize.toUInt16 (a : USize) : UInt16 := a.toNat.toUInt16
+/--
+Converts 32-bit unsigned integers to word-sized unsigned integers.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint32_to_usize"]
 def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.toBitVec.toNat a.toBitVec.isLt
+/--
+Converts word-sized unsigned integers to 32-bit unsigned integers. Wraps around on overflow, which
+might occur on 64-bit architectures.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_to_uint32"]
 def USize.toUInt32 (a : USize) : UInt32 := a.toNat.toUInt32
-/-- Converts a `UInt64` to a `USize` by reducing modulo `USize.size`. -/
+/--
+Converts 64-bit unsigned integers to word-sized unsigned integers. On 32-bit machines, this may
+overflow, which results in the value wrapping around (that is, it is reduced modulo `USize.size`).
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_to_usize"]
 def UInt64.toUSize (a : UInt64) : USize := a.toNat.toUSize
 /--
-Upcast a `USize` to a `UInt64`.
-This is lossless because `USize.size` is either `2^32` or `2^64`.
-This function is overridden with a native implementation.
+Converts word-sized unsigned integers to 32-bit unsigned integers. This cannot overflow because
+`USize.size` is either `2^32` or `2^64`.
+
+This function is overridden at runtime with an efficient implementation.
 -/
 @[extern "lean_usize_to_uint64"]
 def USize.toUInt64 (a : USize) : UInt64 :=
@@ -390,8 +944,21 @@ instance : HMod USize Nat USize := ⟨USize.modn⟩
 
 instance : Div USize       := ⟨USize.div⟩
 
+/--
+Bitwise complement, also known as bitwise negation, for word-sized unsigned integers. Usually
+accessed via the `~~~` prefix operator.
+
+Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_complement"]
 def USize.complement (a : USize) : USize := ⟨~~~a.toBitVec⟩
+/--
+Negation of word-sized unsigned integers, computed modulo `USize.size`.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_neg"]
 def USize.neg (a : USize) : USize := ⟨-a.toBitVec⟩
 

src/Init/Data/UInt/BasicAux.lean

@@ -7,6 +7,8 @@ prelude
 import Init.Data.Fin.Basic
 import Init.Data.BitVec.BasicAux
 
+set_option linter.missingDocs true
+
 /-!
 This module exists to provide the very basic `UInt8` etc. definitions required for
 `Init.Data.Char.Basic` and `Init.Data.Array.Basic`. These are very important as they are used in
@@ -24,6 +26,8 @@ def UInt8.val (x : UInt8) : Fin UInt8.size := x.toFin
 /--
 Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.
 
+This function is overridden at runtime with an efficient implementation.
+
 Examples:
  * `UInt8.ofNat 5 = 5`
  * `UInt8.ofNat 255 = 255`
@@ -33,8 +37,12 @@ Examples:
 -/
 @[extern "lean_uint8_of_nat"]
 def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨BitVec.ofNat 8 n⟩
+
 /--
-Converts the given natural number to `UInt8`, but returns `2^8 - 1` for natural numbers `>= 2^8`.
+Converts a natural number to an 8-bit unsigned integer, returning the largest representable value if
+the number is too large.
+
+Returns `2^8 - 1` for natural numbers greater than or equal to `2^8`.
 -/
 def UInt8.ofNatTruncate (n : Nat) : UInt8 :=
   if h : n < UInt8.size then
@@ -45,6 +53,8 @@ def UInt8.ofNatTruncate (n : Nat) : UInt8 :=
 /--
 Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.
 
+This function is overridden at runtime with an efficient implementation.
+
 Examples:
  * `Nat.toUInt8 5 = 5`
  * `Nat.toUInt8 255 = 255`
@@ -53,6 +63,12 @@ Examples:
  * `Nat.toUInt8 32770 = 2`
 -/
 abbrev Nat.toUInt8 := UInt8.ofNat
+
+/--
+Converts an 8-bit unsigned integer to an arbitrary-precision natural number.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_to_nat"]
 def UInt8.toNat (n : UInt8) : Nat := n.toBitVec.toNat
 
@@ -66,6 +82,8 @@ def UInt16.val (x : UInt16) : Fin UInt16.size := x.toFin
 /--
 Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.
 
+This function is overridden at runtime with an efficient implementation.
+
 Examples:
  * `UInt16.ofNat 5 = 5`
  * `UInt16.ofNat 255 = 255`
@@ -75,7 +93,10 @@ Examples:
 @[extern "lean_uint16_of_nat"]
 def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨BitVec.ofNat 16 n⟩
 /--
-Converts the given natural number to `UInt16`, but returns `2^16 - 1` for natural numbers `>= 2^16`.
+Converts a natural number to a 16-bit unsigned integer, returning the largest representable value if
+the number is too large.
+
+Returns `2^16 - 1` for natural numbers greater than or equal to `2^16`.
 -/
 def UInt16.ofNatTruncate (n : Nat) : UInt16 :=
   if h : n < UInt16.size then
@@ -86,6 +107,8 @@ def UInt16.ofNatTruncate (n : Nat) : UInt16 :=
 /--
 Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.
 
+This function is overridden at runtime with an efficient implementation.
+
 Examples:
  * `Nat.toUInt16 5 = 5`
  * `Nat.toUInt16 255 = 255`
@@ -93,10 +116,26 @@ Examples:
  * `Nat.toUInt16 65537 = 1`
 -/
 abbrev Nat.toUInt16 := UInt16.ofNat
+
+/--
+Converts a 16-bit unsigned integer to an arbitrary-precision natural number.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_to_nat"]
 def UInt16.toNat (n : UInt16) : Nat := n.toBitVec.toNat
+/--
+Converts 16-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_to_uint8"]
 def UInt16.toUInt8 (a : UInt16) : UInt8 := a.toNat.toUInt8
+/--
+Converts 8-bit unsigned integers to 16-bit unsigned integers.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_to_uint16"]
 def UInt8.toUInt16 (a : UInt8) : UInt16 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
 
@@ -110,6 +149,8 @@ def UInt32.val (x : UInt32) : Fin UInt32.size := x.toFin
 /--
 Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.
 
+This function is overridden at runtime with an efficient implementation.
+
 Examples:
  * `UInt32.ofNat 5 = 5`
  * `UInt32.ofNat 65539 = 65539`
@@ -120,7 +161,10 @@ def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨BitVec.ofNat 32 n⟩
 @[inline, deprecated UInt32.ofNatLT (since := "2025-02-13"), inherit_doc UInt32.ofNatLT]
 def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := UInt32.ofNatLT n h
 /--
-Converts the given natural number to `UInt32`, but returns `2^32 - 1` for natural numbers `>= 2^32`.
+Converts a natural number to a 32-bit unsigned integer, returning the largest representable value if
+the number is too large.
+
+Returns `2^32 - 1` for natural numbers greater than or equal to `2^32`.
 -/
 def UInt32.ofNatTruncate (n : Nat) : UInt32 :=
   if h : n < UInt32.size then
@@ -130,18 +174,41 @@ def UInt32.ofNatTruncate (n : Nat) : UInt32 :=
 /--
 Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.
 
+This function is overridden at runtime with an efficient implementation.
+
 Examples:
  * `Nat.toUInt32 5 = 5`
  * `Nat.toUInt32 65_539 = 65_539`
  * `Nat.toUInt32 4_294_967_299 = 3`
 -/
 abbrev Nat.toUInt32 := UInt32.ofNat
+
+/--
+Converts a 32-bit unsigned integer to an 8-bit unsigned integer, wrapping on overflow.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint32_to_uint8"]
 def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8
+/--
+Converts 32-bit unsigned integers to 16-bit unsigned integers. Wraps around on overflow.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint32_to_uint16"]
 def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
+/--
+Converts 8-bit unsigned integers to 32-bit unsigned integers.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_to_uint32"]
 def UInt8.toUInt32 (a : UInt8) : UInt32 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
+/--
+Converts 16-bit unsigned integers to 32-bit unsigned integers.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_to_uint32"]
 def UInt16.toUInt32 (a : UInt16) : UInt32 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
 
@@ -172,6 +239,8 @@ def UInt64.val (x : UInt64) : Fin UInt64.size := x.toFin
 /--
 Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.
 
+This function is overridden at runtime with an efficient implementation.
+
 Examples:
  * `UInt64.ofNat 5 = 5`
  * `UInt64.ofNat 65539 = 65539`
@@ -181,7 +250,10 @@ Examples:
 @[extern "lean_uint64_of_nat"]
 def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨BitVec.ofNat 64 n⟩
 /--
-Converts the given natural number to `UInt64`, but returns `2^64 - 1` for natural numbers `>= 2^64`.
+Converts a natural number to a 64-bit unsigned integer, returning the largest representable value if
+the number is too large.
+
+Returns `2^64 - 1` for natural numbers greater than or equal to `2^64`.
 -/
 def UInt64.ofNatTruncate (n : Nat) : UInt64 :=
   if h : n < UInt64.size then
@@ -191,6 +263,8 @@ def UInt64.ofNatTruncate (n : Nat) : UInt64 :=
 /--
 Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.
 
+This function is overridden at runtime with an efficient implementation.
+
 Examples:
  * `Nat.toUInt64 5 = 5`
  * `Nat.toUInt64 65539 = 65539`
@@ -198,18 +272,53 @@ Examples:
  * `Nat.toUInt64 18_446_744_073_709_551_620 = 4`
 -/
 abbrev Nat.toUInt64 := UInt64.ofNat
+/--
+Converts a 64-bit unsigned integer to an arbitrary-precision natural number.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_to_nat"]
 def UInt64.toNat (n : UInt64) : Nat := n.toBitVec.toNat
+/--
+Converts 64-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_to_uint8"]
 def UInt64.toUInt8 (a : UInt64) : UInt8 := a.toNat.toUInt8
+/--
+Converts 64-bit unsigned integers to 16-bit unsigned integers. Wraps around on overflow.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_to_uint16"]
 def UInt64.toUInt16 (a : UInt64) : UInt16 := a.toNat.toUInt16
+/--
+Converts 64-bit unsigned integers to 32-bit unsigned integers. Wraps around on overflow.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint64_to_uint32"]
 def UInt64.toUInt32 (a : UInt64) : UInt32 := a.toNat.toUInt32
+/--
+Converts 8-bit unsigned integers to 64-bit unsigned integers.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint8_to_uint64"]
 def UInt8.toUInt64 (a : UInt8) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
+/--
+Converts 16-bit unsigned integers to 64-bit unsigned integers. Wraps around on overflow.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint16_to_uint64"]
 def UInt16.toUInt64 (a : UInt16) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
+/--
+Converts 32-bit unsigned integers to 64-bit unsigned integers. Wraps around on overflow.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_uint32_to_uint64"]
 def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
 
@@ -230,12 +339,20 @@ theorem usize_size_pos : 0 < USize.size :=
 def USize.toFin (x : USize) : Fin USize.size := x.toBitVec.toFin
 @[deprecated USize.toFin (since := "2025-02-12"), inherit_doc USize.toFin]
 def USize.val (x : USize) : Fin USize.size := x.toFin
-/-- Converts a natural number to a `USize`, wrapping on overflow. -/
+/--
+Converts an arbitrary-precision natural number to an unsigned word-sized integer, wrapping around on
+overflow.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_of_nat"]
 def USize.ofNat (n : @& Nat) : USize := ⟨BitVec.ofNat _ n⟩
 /--
-Converts the given natural number to `USize`, but returns `USize.size - 1` (i.e., `2^64 - 1` or
-`2^32 - 1` depending on the platform) for natural numbers `>= USize.size`.
+Converts a natural number to `USize`, returning the largest representable value if the number is too
+large.
+
+Returns `USize.size - 1`, which is  `2^64 - 1` or `2^32 - 1` depending on the platform, for natural
+numbers greater than or equal to `USize.size`.
 -/
 def USize.ofNatTruncate (n : Nat) : USize :=
   if h : n < USize.size then
@@ -243,14 +360,39 @@ def USize.ofNatTruncate (n : Nat) : USize :=
   else
     USize.ofNatLT (USize.size - 1) (Nat.pred_lt (Nat.ne_zero_of_lt USize.size_pos))
 @[inherit_doc USize.ofNat] abbrev Nat.toUSize := USize.ofNat
+/--
+Converts a word-sized unsigned integer to an arbitrary-precision natural number.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_to_nat"]
 def USize.toNat (n : USize) : Nat := n.toBitVec.toNat
+/--
+Adds two word-sized unsigned integers, wrapping around on overflow.  Usually accessed via the `+`
+operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_add"]
 def USize.add (a b : USize) : USize := ⟨a.toBitVec + b.toBitVec⟩
+/--
+Subtracts one word-sized-bit unsigned integer from another, wrapping around on underflow. Usually
+accessed via the `-` operator.
+
+This function is overridden at runtime with an efficient implementation.
+-/
 @[extern "lean_usize_sub"]
 def USize.sub (a b : USize) : USize := ⟨a.toBitVec - b.toBitVec⟩
 
+/--
+Strict inequality of word-sized unsigned integers, defined as inequality of the corresponding
+natural numbers. Usually accessed via the `<` operator.
+-/
 def USize.lt (a b : USize) : Prop := a.toBitVec < b.toBitVec
+/--
+Non-strict inequality of word-sized unsigned integers, defined as inequality of the corresponding
+natural numbers. Usually accessed via the `≤` operator.
+-/
 def USize.le (a b : USize) : Prop := a.toBitVec ≤ b.toBitVec
 
 instance USize.instOfNat : OfNat USize n := ⟨USize.ofNat n⟩
@@ -260,10 +402,33 @@ instance : Sub USize       := ⟨USize.sub⟩
 instance : LT USize        := ⟨USize.lt⟩
 instance : LE USize        := ⟨USize.le⟩
 
+/--
+Decides whether one word-sized unsigned integer is strictly less than another. Usually accessed via
+the `DecidableLT USize` instance.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `(if (6 : USize) < 7 then "yes" else "no") = "yes"`
+ * `(if (5 : USize) < 5 then "yes" else "no") = "no"`
+ * `show ¬((7 : USize) < 7) by decide`
+-/
 @[extern "lean_usize_dec_lt"]
 def USize.decLt (a b : USize) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
+/--
+Decides whether one word-sized unsigned integer is less than or equal to another. Usually accessed
+via the `DecidableLE USize` instance.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `(if (15 : USize) ≤ 15 then "yes" else "no") = "yes"`
+ * `(if (15 : USize) ≤ 5 then "yes" else "no") = "no"`
+ * `(if (5 : USize) ≤ 15 then "yes" else "no") = "yes"`
+ * `show (7 : USize) ≤ 7 by decide`
+-/
 @[extern "lean_usize_dec_le"]
 def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))

src/Init/Data/UInt/Log2.lean

@@ -6,17 +6,87 @@ Authors: Henrik Böving
 prelude
 import Init.Data.Fin.Log2
 
+/--
+Base-two logarithm of 8-bit unsigned integers. Returns `⌊max 0 (log₂ a)⌋`.
+
+This function is overridden at runtime with an efficient implementation. This definition is
+the logical model.
+
+Examples:
+ * `UInt8.log2 0 = 0`
+ * `UInt8.log2 1 = 0`
+ * `UInt8.log2 2 = 1`
+ * `UInt8.log2 4 = 2`
+ * `UInt8.log2 7 = 2`
+ * `UInt8.log2 8 = 3`
+-/
 @[extern "lean_uint8_log2"]
 def UInt8.log2 (a : UInt8) : UInt8 := ⟨⟨Fin.log2 a.toFin⟩⟩
 
+/--
+Base-two logarithm of 16-bit unsigned integers. Returns `⌊max 0 (log₂ a)⌋`.
+
+This function is overridden at runtime with an efficient implementation. This definition is
+the logical model.
+
+Examples:
+ * `UInt16.log2 0 = 0`
+ * `UInt16.log2 1 = 0`
+ * `UInt16.log2 2 = 1`
+ * `UInt16.log2 4 = 2`
+ * `UInt16.log2 7 = 2`
+ * `UInt16.log2 8 = 3`
+-/
 @[extern "lean_uint16_log2"]
 def UInt16.log2 (a : UInt16) : UInt16 := ⟨⟨Fin.log2 a.toFin⟩⟩
 
+/--
+Base-two logarithm of 32-bit unsigned integers. Returns `⌊max 0 (log₂ a)⌋`.
+
+This function is overridden at runtime with an efficient implementation. This definition is
+the logical model.
+
+Examples:
+ * `UInt32.log2 0 = 0`
+ * `UInt32.log2 1 = 0`
+ * `UInt32.log2 2 = 1`
+ * `UInt32.log2 4 = 2`
+ * `UInt32.log2 7 = 2`
+ * `UInt32.log2 8 = 3`
+-/
 @[extern "lean_uint32_log2"]
 def UInt32.log2 (a : UInt32) : UInt32 := ⟨⟨Fin.log2 a.toFin⟩⟩
 
+/--
+Base-two logarithm of 64-bit unsigned integers. Returns `⌊max 0 (log₂ a)⌋`.
+
+This function is overridden at runtime with an efficient implementation. This definition is
+the logical model.
+
+Examples:
+ * `UInt64.log2 0 = 0`
+ * `UInt64.log2 1 = 0`
+ * `UInt64.log2 2 = 1`
+ * `UInt64.log2 4 = 2`
+ * `UInt64.log2 7 = 2`
+ * `UInt64.log2 8 = 3`
+-/
 @[extern "lean_uint64_log2"]
 def UInt64.log2 (a : UInt64) : UInt64 := ⟨⟨Fin.log2 a.toFin⟩⟩
 
+/--
+Base-two logarithm of word-sized unsigned integers. Returns `⌊max 0 (log₂ a)⌋`.
+
+This function is overridden at runtime with an efficient implementation. This definition is
+the logical model.
+
+Examples:
+ * `USize.log2 0 = 0`
+ * `USize.log2 1 = 0`
+ * `USize.log2 2 = 1`
+ * `USize.log2 4 = 2`
+ * `USize.log2 7 = 2`
+ * `USize.log2 8 = 3`
+-/
 @[extern "lean_usize_log2"]
 def USize.log2 (a : USize) : USize := ⟨⟨Fin.log2 a.toFin⟩⟩

src/Init/Data/Vector/Attach.lean

@@ -593,8 +593,11 @@ and simplifies these to the function directly taking the value.
   unfold Array.unattach
   rfl
 
-@[simp] theorem unattach_mkVector {p : α → Prop} {n : Nat} {x : { x // p x }} :
-    (mkVector n x).unattach = mkVector n x.1 := by
+@[simp] theorem unattach_replicate {p : α → Prop} {n : Nat} {x : { x // p x }} :
+    (replicate n x).unattach = replicate n x.1 := by
   simp [unattach]
 
+@[deprecated unattach_replicate (since := "2025-03-18")]
+abbrev unattach_mkVector := @unattach_replicate
+
 end Vector

src/Init/Data/Vector/Basic.lean

@@ -67,16 +67,19 @@ def elimAsList {motive : Vector α n → Sort u}
 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⟩
+@[inline] def replicate (n) (v : α) : Vector α n := ⟨Array.replicate n v, by simp⟩
+
+@[deprecated replicate (since := "2025-03-18")]
+abbrev mkVector := @replicate
 
 instance : Nonempty (Vector α 0) := ⟨#v[]⟩
-instance [Nonempty α] : Nonempty (Vector α n) := ⟨mkVector _ Classical.ofNonempty⟩
+instance [Nonempty α] : Nonempty (Vector α n) := ⟨replicate _ Classical.ofNonempty⟩
 
 /-- Returns a vector of size `1` with element `v`. -/
 @[inline] def singleton (v : α) : Vector α 1 := ⟨#[v], rfl⟩
 
 instance [Inhabited α] : Inhabited (Vector α n) where
-  default := mkVector n default
+  default := replicate n default
 
 /-- Get an element of a vector using a `Fin` index. -/
 @[inline] def get (xs : Vector α n) (i : Fin n) : α :=
@@ -471,7 +474,7 @@ Note that we immediately simplify this to an `++` operation,
 and do not provide separate verification theorems.
 -/
 @[inline, simp] def leftpad (n : Nat) (a : α) (xs : Vector α m) : Vector α (max n m) :=
-  (mkVector (n - m) a ++ xs).cast (by omega)
+  (replicate (n - m) a ++ xs).cast (by omega)
 
 /--
 Pad a vector on the right with a given element.
@@ -480,7 +483,7 @@ Note that we immediately simplify this to an `++` operation,
 and do not provide separate verification theorems.
 -/
 @[inline, simp] def rightpad (n : Nat) (a : α) (xs : Vector α m) : Vector α (max n m) :=
-  (xs ++ mkVector (n - m) a).cast (by omega)
+  (xs ++ replicate (n - m) a).cast (by omega)
 
 /-! ### ForIn instance -/
 

src/Init/Data/Vector/Count.lean

@@ -72,10 +72,13 @@ theorem countP_le_size {xs : Vector α n} : countP p xs ≤ n := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-theorem countP_mkVector (p : α → Bool) (a : α) (n : Nat) :
-    countP p (mkVector n a) = if p a then n else 0 := by
-  simp only [mkVector_eq_mk_mkArray, countP_cast, countP_mk]
-  simp [Array.countP_mkArray]
+theorem countP_replicate (p : α → Bool) (a : α) (n : Nat) :
+    countP p (replicate n a) = if p a then n else 0 := by
+  simp only [replicate_eq_mk_replicate, countP_cast, countP_mk]
+  simp [Array.countP_replicate]
+
+@[deprecated countP_replicate (since := "2025-03-18")]
+abbrev countP_mkVector := @countP_replicate
 
 theorem boole_getElem_le_countP (p : α → Bool) (xs : Vector α n) (i : Nat) (h : i < n) :
     (if p xs[i] then 1 else 0) ≤ xs.countP p := by
@@ -217,13 +220,19 @@ theorem count_eq_size {xs : Vector α n} : count a xs = xs.size ↔ ∀ b ∈ xs
   rcases xs with ⟨xs, rfl⟩
   simp [Array.count_eq_size]
 
-@[simp] theorem count_mkVector_self (a : α) (n : Nat) : count a (mkVector n a) = n := by
-  simp only [mkVector_eq_mk_mkArray, count_cast, count_mk]
+@[simp] theorem count_replicate_self (a : α) (n : Nat) : count a (replicate n a) = n := by
+  simp only [replicate_eq_mk_replicate, count_cast, count_mk]
   simp
 
-theorem count_mkVector (a b : α) (n : Nat) : count a (mkVector n b) = if b == a then n else 0 := by
-  simp only [mkVector_eq_mk_mkArray, count_cast, count_mk]
-  simp [Array.count_mkArray]
+@[deprecated count_replicate_self (since := "2025-03-18")]
+abbrev count_mkVector_self := @count_replicate_self
+
+theorem count_replicate (a b : α) (n : Nat) : count a (replicate n b) = if b == a then n else 0 := by
+  simp only [replicate_eq_mk_replicate, count_cast, count_mk]
+  simp [Array.count_replicate]
+
+@[deprecated count_replicate (since := "2025-03-18")]
+abbrev count_mkVector := @count_replicate
 
 theorem count_le_count_map [DecidableEq β] (xs : Vector α n) (f : α → β) (x : α) :
     count x xs ≤ count (f x) (map f xs) := by

src/Init/Data/Vector/Erase.lean

@@ -69,10 +69,13 @@ theorem eraseIdx_cast {xs : Vector α n} {k : Nat} (h : k < m) :
   rcases xs with ⟨xs⟩
   simp
 
-theorem eraseIdx_mkVector {n : Nat} {a : α} {k : Nat} {h} :
-    (mkVector n a).eraseIdx k = mkVector (n - 1) a := by
-  rw [mkVector_eq_mk_mkArray, eraseIdx_mk]
-  simp [Array.eraseIdx_mkArray, *]
+theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} {h} :
+    (replicate n a).eraseIdx k = replicate (n - 1) a := by
+  rw [replicate_eq_mk_replicate, eraseIdx_mk]
+  simp [Array.eraseIdx_replicate, *]
+
+@[deprecated eraseIdx_replicate (since := "2025-03-18")]
+abbrev eraseIdx_mkVector := @eraseIdx_replicate
 
 theorem mem_eraseIdx_iff_getElem {x : α} {xs : Vector α n} {k} {h} : x ∈ xs.eraseIdx k h ↔ ∃ i w, i ≠ k ∧ xs[i]'w = x := by
   rcases xs with ⟨xs⟩

src/Init/Data/Vector/Extract.lean

@@ -131,11 +131,14 @@ theorem extract_append_left {xs : Vector α n} {ys : Vector α m} :
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem extract_mkVector {a : α} {n i j : Nat} :
-    (mkVector n a).extract i j = mkVector (min j n - i) a := by
+@[simp] theorem extract_replicate {a : α} {n i j : Nat} :
+    (replicate n a).extract i j = replicate (min j n - i) a := by
   ext i h
   simp
 
+@[deprecated extract_mkVector (since := "2025-03-18")]
+abbrev extract_mkVector := @extract_replicate
+
 theorem extract_add_left {xs : Vector α n} {i j k : Nat} :
     xs.extract (i + j) k = ((xs.extract i k).extract j (k - i)).cast (by omega) := by
   rcases xs with ⟨xs, rfl⟩

src/Init/Data/Vector/Find.lean

@@ -100,21 +100,33 @@ theorem getElem_zero_flatten {xss : Vector (Vector α m) n} (h : 0 < n * m) :
   simp [getElem?_eq_getElem, h] at t
   simp [← t]
 
-theorem findSome?_mkVector : findSome? f (mkVector n a) = if n = 0 then none else f a := by
-  rw [mkVector_eq_mk_mkArray, findSome?_mk, Array.findSome?_mkArray]
+theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
+  rw [replicate_eq_mk_replicate, findSome?_mk, Array.findSome?_replicate]
 
-@[simp] theorem findSome?_mkVector_of_pos (h : 0 < n) : findSome? f (mkVector n a) = f a := by
-  simp [findSome?_mkVector, Nat.ne_of_gt h]
+@[deprecated findSome?_replicate (since := "2025-03-18")]
+abbrev findSome?_mkVector := @findSome?_replicate
+
+@[simp] theorem findSome?_replicate_of_pos (h : 0 < n) : findSome? f (replicate n a) = f a := by
+  simp [findSome?_replicate, Nat.ne_of_gt h]
+
+@[deprecated findSome?_replicate_of_pos (since := "2025-03-18")]
+abbrev findSome?_mkVector_of_pos := @findSome?_replicate_of_pos
 
 -- Argument is unused, but used to decide whether `simp` should unfold.
-@[simp] theorem findSome?_mkVector_of_isSome (_ : (f a).isSome) :
-   findSome? f (mkVector n a) = if n = 0 then none else f a := by
-  simp [findSome?_mkVector]
+@[simp] theorem findSome?_replicate_of_isSome (_ : (f a).isSome) :
+   findSome? f (replicate n a) = if n = 0 then none else f a := by
+  simp [findSome?_replicate]
 
-@[simp] theorem findSome?_mkVector_of_isNone (h : (f a).isNone) :
-    findSome? f (mkVector n a) = none := by
+@[deprecated findSome?_replicate_of_isSome (since := "2025-03-18")]
+abbrev findSome?_mkVector_of_isSome := @findSome?_replicate_of_isSome
+
+@[simp] theorem findSome?_replicate_of_isNone (h : (f a).isNone) :
+    findSome? f (replicate n a) = none := by
   rw [Option.isNone_iff_eq_none] at h
-  simp [findSome?_mkVector, h]
+  simp [findSome?_replicate, h]
+
+@[deprecated findSome?_replicate_of_isNone (since := "2025-03-18")]
+abbrev findSome?_mkVector_of_isNone := @findSome?_replicate_of_isNone
 
 /-! ### find? -/
 
@@ -211,36 +223,57 @@ theorem find?_flatMap_eq_none_iff {xs : Vector α n} {f : α → Vector β m} {p
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
-theorem find?_mkVector :
-    find? p (mkVector n a) = if n = 0 then none else if p a then some a else none := by
-  rw [mkVector_eq_mk_mkArray, find?_mk, Array.find?_mkArray]
+theorem find?_replicate :
+    find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
+  rw [replicate_eq_mk_replicate, find?_mk, Array.find?_replicate]
 
-@[simp] theorem find?_mkVector_of_length_pos (h : 0 < n) :
-    find? p (mkVector n a) = if p a then some a else none := by
-  simp [find?_mkVector, Nat.ne_of_gt h]
+@[deprecated find?_replicate (since := "2025-03-18")]
+abbrev find?_mkVector := @find?_replicate
 
-@[simp] theorem find?_mkVector_of_pos (h : p a) :
-    find? p (mkVector n a) = if n = 0 then none else some a := by
-  simp [find?_mkVector, h]
+@[simp] theorem find?_replicate_of_size_pos (h : 0 < n) :
+    find? p (replicate n a) = if p a then some a else none := by
+  simp [find?_replicate, Nat.ne_of_gt h]
 
-@[simp] theorem find?_mkVector_of_neg (h : ¬ p a) : find? p (mkVector n a) = none := by
-  simp [find?_mkVector, h]
+@[deprecated find?_replicate_of_size_pos (since := "2025-03-18")]
+abbrev find?_mkVector_of_length_pos := @find?_replicate_of_size_pos
+
+@[simp] theorem find?_replicate_of_pos (h : p a) :
+    find? p (replicate n a) = if n = 0 then none else some a := by
+  simp [find?_replicate, h]
+
+@[deprecated find?_replicate_of_pos (since := "2025-03-18")]
+abbrev find?_mkVector_of_pos := @find?_replicate_of_pos
+
+@[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
+  simp [find?_replicate, h]
+
+@[deprecated find?_replicate_of_neg (since := "2025-03-18")]
+abbrev find?_mkVector_of_neg := @find?_replicate_of_neg
 
 -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
-theorem find?_mkVector_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
-    (mkVector n a).find? p = none ↔ n = 0 ∨ !p a := by
+theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
+    (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
   simp [Classical.or_iff_not_imp_left]
 
-@[simp] theorem find?_mkVector_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
-    (mkVector n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
-  rw [mkVector_eq_mk_mkArray, find?_mk]
+@[deprecated find?_replicate_eq_none_iff (since := "2025-03-18")]
+abbrev find?_mkVector_eq_none_iff := @find?_replicate_eq_none_iff
+
+@[simp] theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
+    (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
+  rw [replicate_eq_mk_replicate, find?_mk]
   simp
 
-@[simp] theorem get_find?_mkVector (n : Nat) (a : α) (p : α → Bool) (h) :
-    ((mkVector n a).find? p).get h = a := by
-  simp only [mkVector_eq_mk_mkArray, find?_mk]
+@[deprecated find?_replicate_eq_some_iff (since := "2025-03-18")]
+abbrev find?_mkVector_eq_some_iff := @find?_replicate_eq_some_iff
+
+@[simp] theorem get_find?_replicate (n : Nat) (a : α) (p : α → Bool) (h) :
+    ((replicate n a).find? p).get h = a := by
+  simp only [replicate_eq_mk_replicate, find?_mk]
   simp
 
+@[deprecated get_find?_replicate (since := "2025-03-18")]
+abbrev get_find?_mkVector := @get_find?_replicate
+
 theorem find?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Vector α n)
     (H : ∀ (a : α), a ∈ xs → P a) (p : β → Bool) :
     (xs.pmap f H).find? p = (xs.attach.find? (fun ⟨a, m⟩ => p (f a (H a m)))).map fun ⟨a, m⟩ => f a (H a m) := by

src/Init/Data/Vector/Lemmas.lean

@@ -465,7 +465,10 @@ theorem toArray_mapM_go [Monad m] [LawfulMonad m] (f : α → m β) (xs : Vector
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem toArray_mkVector : (mkVector n a).toArray = mkArray n a := rfl
+@[simp] theorem toArray_replicate : (replicate n a).toArray = Array.replicate n a := rfl
+
+@[deprecated toArray_replicate (since := "2025-03-18")]
+abbrev toArray_mkVector := @toArray_replicate
 
 @[simp] theorem toArray_inj {xs ys : Vector α n} : xs.toArray = ys.toArray ↔ xs = ys := by
   cases xs
@@ -642,7 +645,10 @@ theorem toList_swap (xs : Vector α n) (i j) (hi hj) :
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem toList_mkVector : (mkVector n a).toList = List.replicate n a := rfl
+@[simp] theorem toList_replicate : (replicate n a).toList = List.replicate n a := rfl
+
+@[deprecated toList_replicate (since := "2025-03-18")]
+abbrev toList_mkVector := @toList_replicate
 
 theorem toList_inj {xs ys : Vector α n} : xs.toList = ys.toList ↔ xs = ys := by
   cases xs
@@ -758,23 +764,38 @@ theorem singleton_inj : #v[a] = #v[b] ↔ a = b := by
   · rintro rfl
     simp
 
-/-! ### mkVector -/
+/-! ### replicate -/
 
-@[simp] theorem mkVector_zero : mkVector 0 a = #v[] := rfl
+@[simp] theorem replicate_zero : replicate 0 a = #v[] := rfl
 
-theorem mkVector_succ : mkVector (n + 1) a = (mkVector n a).push a := by
-  simp [mkVector, Array.mkArray_succ]
+@[deprecated replicate_zero (since := "2025-03-18")]
+abbrev replicate_mkVector := @replicate_zero
 
-@[simp] theorem mkVector_inj : mkVector n a = mkVector n b ↔ n = 0 ∨ a = b := by
-  simp [← toArray_inj, toArray_mkVector, Array.mkArray_inj]
+theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by
+  simp [replicate, Array.replicate_succ]
 
-@[simp] theorem _root_.Array.mk_mkArray (a : α) (n : Nat) (h : (mkArray n a).size = m) :
-    mk (Array.mkArray n a) h = (mkVector n a).cast (by simpa using h) := rfl
+@[deprecated replicate_succ (since := "2025-03-18")]
+abbrev replicate_mkVector_succ := @replicate_succ
 
-theorem mkVector_eq_mk_mkArray (a : α) (n : Nat) :
-    mkVector n a = mk (mkArray n a) (by simp) := by
+@[simp] theorem replicate_inj : replicate n a = replicate n b ↔ n = 0 ∨ a = b := by
+  simp [← toArray_inj, toArray_replicate, Array.replicate_inj]
+
+@[deprecated replicate_inj (since := "2025-03-18")]
+abbrev mkVector_inj := @replicate_inj
+
+@[simp] theorem _root_.Array.vector_mk_replicate (a : α) (n : Nat) :
+    mk (n := n) (Array.replicate n a) (by simp) = replicate n a := rfl
+
+@[deprecated _root_.Array.vector_mk_replicate (since := "2025-03-18")]
+abbrev _root_.Array.mk_mkArray := @_root_.Array.vector_mk_replicate
+
+theorem replicate_eq_mk_replicate (a : α) (n : Nat) :
+    replicate n a = mk (n := n) (Array.replicate n a) (by simp) := by
   simp
 
+@[deprecated replicate_eq_mk_replicate (since := "2025-03-18")]
+abbrev mkVector_eq_mk_mkArray := @replicate_eq_mk_replicate
+
 /-! ## L[i] and L[i]? -/
 
 @[simp] theorem getElem?_eq_none_iff {xs : Vector α n} : xs[i]? = none ↔ n ≤ i := by
@@ -1294,15 +1315,18 @@ theorem mem_setIfInBounds (xs : Vector α n) (i : Nat) (hi : i < n) (a : α) :
   cases ys
   simp
 
-@[simp] theorem mkVector_beq_mkVector [BEq α] {a b : α} {n : Nat} :
-    (mkVector n a == mkVector n b) = (n == 0 || a == b) := by
+@[simp] theorem replicate_beq_replicate [BEq α] {a b : α} {n : Nat} :
+    (replicate n a == replicate n b) = (n == 0 || a == b) := by
   cases n with
   | zero => simp
   | succ n =>
-    rw [mkVector_succ, mkVector_succ, push_beq_push, mkVector_beq_mkVector]
+    rw [replicate_succ, replicate_succ, push_beq_push, replicate_beq_replicate]
     rw [Bool.eq_iff_iff]
     simp +contextual
 
+@[deprecated replicate_beq_replicate (since := "2025-03-18")]
+abbrev mkVector_beq_mkVector := @replicate_beq_replicate
+
 @[simp] theorem reflBEq_iff [BEq α] [NeZero n] : ReflBEq (Vector α n) ↔ ReflBEq α := by
   match n, NeZero.ne n with
   | n + 1, _ =>
@@ -1310,8 +1334,8 @@ theorem mem_setIfInBounds (xs : Vector α n) (i : Nat) (hi : i < n) (a : α) :
     · intro h
       constructor
       intro a
-      suffices (mkVector (n + 1) a == mkVector (n + 1) a) = true by
-        rw [mkVector_succ, push_beq_push, Bool.and_eq_true] at this
+      suffices (replicate (n + 1) a == replicate (n + 1) a) = true by
+        rw [replicate_succ, push_beq_push, Bool.and_eq_true] at this
         exact this.2
       simp
     · intro h
@@ -1326,15 +1350,15 @@ theorem mem_setIfInBounds (xs : Vector α n) (i : Nat) (hi : i < n) (a : α) :
     · intro h
       constructor
       · intro a b h
-        have := mkVector_inj (n := n+1) (a := a) (b := b)
+        have := replicate_inj (n := n+1) (a := a) (b := b)
         simp only [Nat.add_one_ne_zero, false_or] at this
         rw [← this]
         apply eq_of_beq
-        rw [mkVector_beq_mkVector]
+        rw [replicate_beq_replicate]
         simpa
       · intro a
-        suffices (mkVector (n + 1) a == mkVector (n + 1) a) = true by
-          rw [mkVector_beq_mkVector] at this
+        suffices (replicate (n + 1) a == replicate (n + 1) a) = true by
+          rw [replicate_beq_replicate] at this
           simpa
         simp
     · intro h
@@ -1438,8 +1462,8 @@ theorem map_inj [NeZero n] : map (n := n) f = map g ↔ f = g := by
   constructor
   · intro h
     ext a
-    replace h := congrFun h (mkVector n a)
-    simp only [mkVector, map_mk, mk.injEq, Array.map_inj_left, Array.mem_mkArray,  and_imp,
+    replace h := congrFun h (replicate n a)
+    simp only [replicate, map_mk, mk.injEq, Array.map_inj_left, Array.mem_replicate,  and_imp,
       forall_eq_apply_imp_iff] at h
     exact h (NeZero.ne n)
   · intro h; subst h; rfl
@@ -1957,104 +1981,169 @@ theorem map_eq_flatMap {α β} (f : α → β) (xs : Vector α n) :
   rcases xs with ⟨xs, rfl⟩
   simp [Array.map_eq_flatMap]
 
-/-! ### mkVector -/
+/-! ### replicate -/
 
-@[simp] theorem mkVector_one : mkVector 1 a = #v[a] := rfl
+@[simp] theorem replicate_one : replicate 1 a = #v[a] := rfl
 
-/-- Variant of `mkVector_succ` that prepends `a` at the beginning of the vector. -/
-theorem mkVector_succ' : mkVector (n + 1) a = (#v[a] ++ mkVector n a).cast (by omega) := by
+@[deprecated replicate_one (since := "2025-03-18")]
+abbrev replicate_mkVector_one := @replicate_one
+
+/-- Variant of `replicate_succ` that prepends `a` at the beginning of the vector. -/
+theorem replicate_succ' : replicate (n + 1) a = (#v[a] ++ replicate n a).cast (by omega) := by
   rw [← toArray_inj]
-  simp [Array.mkArray_succ']
+  simp [Array.replicate_succ']
 
-@[simp] theorem mem_mkVector {a b : α} {n} : b ∈ mkVector n a ↔ n ≠ 0 ∧ b = a := by
-  unfold mkVector
+@[deprecated replicate_succ' (since := "2025-03-18")]
+abbrev mkVector_succ' := @replicate_succ'
+
+@[simp] theorem mem_replicate {a b : α} {n} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by
+  unfold replicate
   simp only [mem_mk]
   simp
 
-theorem eq_of_mem_mkVector {a b : α} {n} (h : b ∈ mkVector n a) : b = a := (mem_mkVector.1 h).2
+@[deprecated mem_replicate (since := "2025-03-18")]
+abbrev mem_mkVector := @mem_replicate
 
-theorem forall_mem_mkVector {p : α → Prop} {a : α} {n} :
-    (∀ b, b ∈ mkVector n a → p b) ↔ n = 0 ∨ p a := by
-  cases n <;> simp [mem_mkVector]
+theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a := (mem_replicate.1 h).2
 
-@[simp] theorem getElem_mkVector (a : α) (n i : Nat) (h : i < n) : (mkVector n a)[i] = a := by
-  rw [mkVector_eq_mk_mkArray, getElem_mk]
+@[deprecated eq_of_mem_replicate (since := "2025-03-18")]
+abbrev eq_of_mem_mkVector := @eq_of_mem_replicate
+
+theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
+    (∀ b, b ∈ replicate n a → p b) ↔ n = 0 ∨ p a := by
+  cases n <;> simp [mem_replicate]
+
+@[deprecated forall_mem_replicate (since := "2025-03-18")]
+abbrev forall_mem_mkVector := @forall_mem_replicate
+
+@[simp] theorem getElem_replicate (a : α) (n i : Nat) (h : i < n) : (replicate n a)[i] = a := by
+  rw [replicate_eq_mk_replicate, getElem_mk]
   simp
 
-theorem getElem?_mkVector (a : α) (n i : Nat) : (mkVector n a)[i]? = if i < n then some a else none := by
+@[deprecated getElem_replicate (since := "2025-03-18")]
+abbrev getElem_mkVector := @getElem_replicate
+
+theorem getElem?_replicate (a : α) (n i : Nat) : (replicate n a)[i]? = if i < n then some a else none := by
   simp [getElem?_def]
 
-@[simp] theorem getElem?_mkVector_of_lt {n : Nat} {i : Nat} (h : i < n) : (mkVector n a)[i]? = some a := by
-  simp [getElem?_mkVector, h]
+@[deprecated getElem?_replicate (since := "2025-03-18")]
+abbrev getElem?_mkVector := @getElem?_replicate
 
-theorem eq_mkVector_of_mem {a : α} {xs : Vector α n} (h : ∀ (b) (_ : b ∈ xs), b = a) : xs = mkVector n a := by
+@[simp] theorem getElem?_replicate_of_lt {n : Nat} {i : Nat} (h : i < n) : (replicate n a)[i]? = some a := by
+  simp [getElem?_replicate, h]
+
+@[deprecated getElem?_replicate_of_lt (since := "2025-03-18")]
+abbrev getElem?_mkVector_of_lt := @getElem?_replicate_of_lt
+
+theorem eq_replicate_of_mem {a : α} {xs : Vector α n} (h : ∀ (b) (_ : b ∈ xs), b = a) : xs = replicate n a := by
   rw [← toArray_inj]
-  simpa using Array.eq_mkArray_of_mem (xs := xs.toArray) (by simpa using h)
+  simpa using Array.eq_replicate_of_mem (xs := xs.toArray) (by simpa using h)
 
-theorem eq_mkVector_iff {a : α} {n} {xs : Vector α n} :
-    xs = mkVector n a ↔ ∀ (b) (_ : b ∈ xs), b = a := by
+@[deprecated eq_replicate_of_mem (since := "2025-03-18")]
+abbrev eq_mkVector_of_mem := @eq_replicate_of_mem
+
+theorem eq_replicate_iff {a : α} {n} {xs : Vector α n} :
+    xs = replicate n a ↔ ∀ (b) (_ : b ∈ xs), b = a := by
   rw [← toArray_inj]
-  simpa using Array.eq_mkArray_iff (xs := xs.toArray) (n := n)
+  simpa using Array.eq_replicate_iff (xs := xs.toArray) (n := n)
 
-theorem map_eq_mkVector_iff {xs : Vector α n} {f : α → β} {b : β} :
-    xs.map f = mkVector n b ↔ ∀ x ∈ xs, f x = b := by
-  simp [eq_mkVector_iff]
+@[deprecated eq_replicate_iff (since := "2025-03-18")]
+abbrev eq_mkVector_iff := @eq_replicate_iff
 
-@[simp] theorem map_const (xs : Vector α n) (b : β) : map (Function.const α b) xs = mkVector n b :=
-  map_eq_mkVector_iff.mpr fun _ _ => rfl
+theorem map_eq_replicate_iff {xs : Vector α n} {f : α → β} {b : β} :
+    xs.map f = replicate n b ↔ ∀ x ∈ xs, f x = b := by
+  simp [eq_replicate_iff]
 
-@[simp] theorem map_const_fun (x : β) : map (n := n) (Function.const α x) = fun _ => mkVector n x := by
+@[deprecated map_eq_replicate_iff (since := "2025-03-18")]
+abbrev map_eq_mkVector_iff := @map_eq_replicate_iff
+
+@[simp] theorem map_const (xs : Vector α n) (b : β) : map (Function.const α b) xs = replicate n b :=
+  map_eq_replicate_iff.mpr fun _ _ => rfl
+
+@[simp] theorem map_const_fun (x : β) : map (n := n) (Function.const α x) = fun _ => replicate n x := by
   funext xs
   simp
 
 /-- Variant of `map_const` using a lambda rather than `Function.const`. -/
 -- This can not be a `@[simp]` lemma because it would fire on every `List.map`.
-theorem map_const' (xs : Vector α n) (b : β) : map (fun _ => b) xs = mkVector n b :=
+theorem map_const' (xs : Vector α n) (b : β) : map (fun _ => b) xs = replicate n b :=
   map_const xs b
 
-@[simp] theorem set_mkVector_self : (mkVector n a).set i a h = mkVector n a := by
+@[simp] theorem set_replicate_self : (replicate n a).set i a h = replicate n a := by
   rw [← toArray_inj]
   simp
 
-@[simp] theorem setIfInBounds_mkVector_self : (mkVector n a).setIfInBounds i a = mkVector n a := by
+@[deprecated set_replicate_self (since := "2025-03-18")]
+abbrev set_mkVector_self := @set_replicate_self
+
+@[simp] theorem setIfInBounds_replicate_self : (replicate n a).setIfInBounds i a = replicate n a := by
   rw [← toArray_inj]
   simp
 
-@[simp] theorem mkVector_append_mkVector : mkVector n a ++ mkVector m a = mkVector (n + m) a := by
+@[deprecated setIfInBounds_replicate_self (since := "2025-03-18")]
+abbrev setIfInBounds_mkVector_self := @setIfInBounds_replicate_self
+
+@[simp] theorem replicate_append_replicate : replicate n a ++ replicate m a = replicate (n + m) a := by
   rw [← toArray_inj]
   simp
 
-theorem append_eq_mkVector_iff {xs : Vector α n} {ys : Vector α m} {a : α} :
-    xs ++ ys = mkVector (n + m) a ↔ xs = mkVector n a ∧ ys = mkVector m a := by
-  simp [← toArray_inj, Array.append_eq_mkArray_iff]
+@[deprecated replicate_append_replicate (since := "2025-03-18")]
+abbrev mkVector_append_mkVector := @replicate_append_replicate
 
-theorem mkVector_eq_append_iff {xs : Vector α n} {ys : Vector α m} {a : α} :
-    mkVector (n + m) a = xs ++ ys ↔ xs = mkVector n a ∧ ys = mkVector m a := by
-  rw [eq_comm, append_eq_mkVector_iff]
+theorem append_eq_replicate_iff {xs : Vector α n} {ys : Vector α m} {a : α} :
+    xs ++ ys = replicate (n + m) a ↔ xs = replicate n a ∧ ys = replicate m a := by
+  simp [← toArray_inj, Array.append_eq_replicate_iff]
 
-@[simp] theorem map_mkVector : (mkVector n a).map f = mkVector n (f a) := by
+@[deprecated append_eq_replicate_iff (since := "2025-03-18")]
+abbrev append_eq_mkVector_iff := @append_eq_replicate_iff
+
+theorem replicate_eq_append_iff {xs : Vector α n} {ys : Vector α m} {a : α} :
+    replicate (n + m) a = xs ++ ys ↔ xs = replicate n a ∧ ys = replicate m a := by
+  rw [eq_comm, append_eq_replicate_iff]
+
+@[deprecated replicate_eq_append_iff (since := "2025-03-18")]
+abbrev mkVector_eq_append_iff := @replicate_eq_append_iff
+
+@[simp] theorem map_replicate : (replicate n a).map f = replicate n (f a) := by
   rw [← toArray_inj]
   simp
 
+@[deprecated map_replicate (since := "2025-03-18")]
+abbrev map_mkVector := @map_replicate
 
-@[simp] theorem flatten_mkVector_empty : (mkVector n (#v[] : Vector α 0)).flatten = #v[] := by
+@[simp] theorem flatten_replicate_empty : (replicate n (#v[] : Vector α 0)).flatten = #v[] := by
   rw [← toArray_inj]
   simp
 
-@[simp] theorem flatten_mkVector_singleton : (mkVector n #v[a]).flatten = (mkVector n a).cast (by simp) := by
+@[deprecated flatten_replicate_empty (since := "2025-03-18")]
+abbrev flatten_mkVector_empty := @flatten_replicate_empty
+
+@[simp] theorem flatten_replicate_singleton : (replicate n #v[a]).flatten = (replicate n a).cast (by simp) := by
   ext i h
   simp [h]
 
-@[simp] theorem flatten_mkVector_mkVector : (mkVector n (mkVector m a)).flatten = mkVector (n * m) a := by
+@[deprecated flatten_replicate_singleton (since := "2025-03-18")]
+abbrev flatten_mkVector_singleton := @flatten_replicate_singleton
+
+@[simp] theorem flatten_replicate_replicate : (replicate n (replicate m a)).flatten = replicate (n * m) a := by
   ext i h
   simp [h]
 
-theorem flatMap_mkArray {β} (f : α → Vector β m) : (mkVector n a).flatMap f = (mkVector n (f a)).flatten := by
+@[deprecated flatten_replicate_replicate (since := "2025-03-18")]
+abbrev flatten_mkVector_mkVector := @flatten_replicate_replicate
+
+theorem flatMap_replicate {β} (f : α → Vector β m) : (replicate n a).flatMap f = (replicate n (f a)).flatten := by
   ext i h
   simp [h]
 
-@[simp] theorem sum_mkArray_nat (n : Nat) (a : Nat) : (mkVector n a).sum = n * a := by
-  simp [toArray_mkVector]
+@[deprecated flatMap_replicate (since := "2025-03-18")]
+abbrev flatMap_mkVector := @flatMap_replicate
+
+@[simp] theorem sum_replicate_nat (n : Nat) (a : Nat) : (replicate n a).sum = n * a := by
+  simp [toArray_replicate]
+
+@[deprecated sum_replicate_nat (since := "2025-03-18")]
+abbrev sum_mkVector := @sum_replicate_nat
 
 /-! ### reverse -/
 
@@ -2148,10 +2237,13 @@ theorem flatMap_reverse {β} (xs : Vector α n) (f : α → Vector β m) :
   rcases xs with ⟨xs, rfl⟩
   simp [Array.flatMap_reverse, Function.comp_def]
 
-@[simp] theorem reverse_mkVector (n) (a : α) : reverse (mkVector n a) = mkVector n a := by
+@[simp] theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a := by
   rw [← toArray_inj]
   simp
 
+@[deprecated reverse_replicate (since := "2025-03-18")]
+abbrev reverse_mkVector := @reverse_replicate
+
 /-! ### extract -/
 
 @[simp] theorem getElem_extract {as : Vector α n} {start stop : Nat}
@@ -2454,14 +2546,20 @@ theorem back?_flatten {xss : Vector (Vector α m) n} :
   simp [Array.back?_flatten, ← Array.map_reverse, Array.findSome?_map, Function.comp_def]
   rfl
 
-theorem back?_mkVector (a : α) (n : Nat) :
-    (mkVector n a).back? = if n = 0 then none else some a := by
-  rw [mkVector_eq_mk_mkArray]
-  simp only [back?_mk, Array.back?_mkArray]
+theorem back?_replicate (a : α) (n : Nat) :
+    (replicate n a).back? = if n = 0 then none else some a := by
+  rw [replicate_eq_mk_replicate]
+  simp only [back?_mk, Array.back?_replicate]
 
-@[simp] theorem back_mkArray [NeZero n] : (mkVector n a).back = a := by
+@[deprecated back?_replicate (since := "2025-03-18")]
+abbrev back?_mkVector := @back?_replicate
+
+@[simp] theorem back_replicate [NeZero n] : (replicate n a).back = a := by
   simp [back_eq_getElem]
 
+@[deprecated back_replicate (since := "2025-03-18")]
+abbrev back_mkVector := @back_replicate
+
 /-! ### leftpad and rightpad -/
 
 @[simp] theorem leftpad_mk (n : Nat) (a : α) (xs : Array α) (h : xs.size = m) :
@@ -2539,9 +2637,12 @@ theorem pop_append {xs : Vector α n} {ys : Vector α m} :
   rw [Array.pop_append]
   split <;> simp_all
 
-@[simp] theorem pop_mkVector (n) (a : α) : (mkVector n a).pop = mkVector (n - 1) a := by
+@[simp] theorem pop_replicate (n) (a : α) : (replicate n a).pop = replicate (n - 1) a := by
   ext <;> simp
 
+@[deprecated pop_replicate (since := "2025-03-18")]
+abbrev pop_mkVector := @pop_replicate
+
 /-! ### replace -/
 
 section replace
@@ -2605,16 +2706,22 @@ theorem replace_extract {xs : Vector α n} {i : Nat} :
   rcases xs with ⟨xs, rfl⟩
   simp [Array.replace_extract]
 
-@[simp] theorem replace_mkArray_self {a : α} (h : 0 < n) :
-    (mkVector n a).replace a b = (#v[b] ++ mkVector (n - 1) a).cast (by omega) := by
+@[simp] theorem replace_replicate_self {a : α} (h : 0 < n) :
+    (replicate n a).replace a b = (#v[b] ++ replicate (n - 1) a).cast (by omega) := by
   match n, h with
-  | n + 1, _ => simp_all [mkVector_succ', replace_append]
+  | n + 1, _ => simp_all [replicate_succ', replace_append]
 
-@[simp] theorem replace_mkArray_ne {a b c : α} (h : !b == a) :
-    (mkVector n a).replace b c = mkVector n a := by
+@[deprecated replace_replicate_self (since := "2025-03-18")]
+abbrev replace_mkArray_self := @replace_replicate_self
+
+@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
+    (replicate n a).replace b c = replicate n a := by
   rw [replace_of_not_mem]
   simp_all
 
+@[deprecated replace_replicate_ne (since := "2025-03-18")]
+abbrev replace_mkArray_ne := @replace_replicate_ne
+
 end replace
 
 /-! ## Logic -/
@@ -2764,13 +2871,19 @@ theorem any_eq_not_all_not (xs : Vector α n) (p : α → Bool) : xs.any p = !xs
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem any_mkVector {n : Nat} {a : α} :
-    (mkVector n a).any f = if n = 0 then false else f a := by
-  induction n <;> simp_all [mkVector_succ']
+@[simp] theorem any_replicate {n : Nat} {a : α} :
+    (replicate n a).any f = if n = 0 then false else f a := by
+  induction n <;> simp_all [replicate_succ']
 
-@[simp] theorem all_mkVector {n : Nat} {a : α} :
-    (mkVector n a).all f = if n = 0 then true else f a := by
-  induction n <;> simp_all +contextual [mkVector_succ']
+@[deprecated any_replicate (since := "2025-03-18")]
+abbrev any_mkVector := @any_replicate
+
+@[simp] theorem all_replicate {n : Nat} {a : α} :
+    (replicate n a).all f = if n = 0 then true else f a := by
+  induction n <;> simp_all +contextual [replicate_succ']
+
+@[deprecated all_replicate (since := "2025-03-18")]
+abbrev all_mkVector := @all_replicate
 
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 

src/Init/Data/Vector/MapIdx.lean

@@ -217,10 +217,13 @@ theorem mapFinIdx_eq_mapFinIdx_iff {xs : Vector α n} {f g : (i : Nat) → α
     (xs.mapFinIdx f).mapFinIdx g = xs.mapFinIdx (fun i a h => g i (f i a h) h) := by
   simp [mapFinIdx_eq_iff]
 
-theorem mapFinIdx_eq_mkVector_iff {xs : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} {b : β} :
-    xs.mapFinIdx f = mkVector n b ↔ ∀ (i : Nat) (h : i < n), f i xs[i] h = b := by
+theorem mapFinIdx_eq_replicate_iff {xs : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} {b : β} :
+    xs.mapFinIdx f = replicate n b ↔ ∀ (i : Nat) (h : i < n), f i xs[i] h = b := by
   rcases xs with ⟨xs, rfl⟩
-  simp [Array.mapFinIdx_eq_mkArray_iff]
+  simp [Array.mapFinIdx_eq_replicate_iff]
+
+@[deprecated mapFinIdx_eq_replicate_iff (since := "2025-03-18")]
+abbrev mapFinIdx_eq_mkVector_iff := @mapFinIdx_eq_replicate_iff
 
 @[simp] theorem mapFinIdx_reverse {xs : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
     xs.reverse.mapFinIdx f = (xs.mapFinIdx (fun i a h => f (n - 1 - i) a (by omega))).reverse := by
@@ -350,10 +353,13 @@ theorem mapIdx_eq_mapIdx_iff {xs : Vector α n} :
     (xs.mapIdx f).mapIdx g = xs.mapIdx (fun i => g i ∘ f i) := by
   simp [mapIdx_eq_iff]
 
-theorem mapIdx_eq_mkVector_iff {xs : Vector α n} {f : Nat → α → β} {b : β} :
-    mapIdx f xs = mkVector n b ↔ ∀ (i : Nat) (h : i < n), f i xs[i] = b := by
+theorem mapIdx_eq_replicate_iff {xs : Vector α n} {f : Nat → α → β} {b : β} :
+    mapIdx f xs = replicate n b ↔ ∀ (i : Nat) (h : i < n), f i xs[i] = b := by
   rcases xs with ⟨xs, rfl⟩
-  simp [Array.mapIdx_eq_mkArray_iff]
+  simp [Array.mapIdx_eq_replicate_iff]
+
+@[deprecated mapIdx_eq_replicate_iff (since := "2025-03-18")]
+abbrev mapIdx_eq_mkVector_iff := @mapIdx_eq_replicate_iff
 
 @[simp] theorem mapIdx_reverse {xs : Vector α n} {f : Nat → α → β} :
     xs.reverse.mapIdx f = (mapIdx (fun i => f (xs.size - 1 - i)) xs).reverse := by

src/Init/Data/Vector/Zip.lean

@@ -144,11 +144,14 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {as : Vector α (n + m)} {b
     simp only at w₁ w₂
     exact ⟨as₁, as₂, bs₁, bs₂, by simpa [hw, hy] using ⟨w₁, w₂⟩⟩
 
-@[simp] theorem zipWith_mkVector {a : α} {b : β} {n : Nat} :
-    zipWith f (mkVector n a) (mkVector n b) = mkVector n (f a b) := by
+@[simp] theorem zipWith_replicate {a : α} {b : β} {n : Nat} :
+    zipWith f (replicate n a) (replicate n b) = replicate n (f a b) := by
   ext
   simp
 
+@[deprecated zipWith_replicate (since := "2025-03-18")]
+abbrev zipWith_mkVector := @zipWith_replicate
+
 theorem map_uncurry_zip_eq_zipWith (f : α → β → γ) (as : Vector α n) (bs : Vector β n) :
     map (Function.uncurry f) (as.zip bs) = zipWith f as bs := by
   rcases as with ⟨as, rfl⟩
@@ -240,10 +243,12 @@ theorem zip_eq_append_iff {as : Vector α (n + m)} {bs : Vector β (n + m)} {xs
       ∃ as₁ as₂ bs₁ bs₂, as₁.size = bs₁.size ∧ as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = zip as₁ bs₁ ∧ ys = zip as₂ bs₂ := by
   simp [zip_eq_zipWith, zipWith_eq_append_iff]
 
-@[simp] theorem zip_mkVector {a : α} {b : β} {n : Nat} :
-    zip (mkVector n a) (mkVector n b) = mkVector n (a, b) := by
+@[simp] theorem zip_replicate {a : α} {b : β} {n : Nat} :
+    zip (replicate n a) (replicate n b) = replicate n (a, b) := by
   ext <;> simp
 
+@[deprecated zip_replicate (since := "2025-03-18")]
+abbrev zip_mkVector := @zip_replicate
 
 /-! ### unzip -/
 
@@ -285,8 +290,11 @@ theorem zip_of_prod {as : Vector α n} {bs : Vector β n} {xs : Vector (α × β
     (hr : xs.map Prod.snd = bs) : xs = as.zip bs := by
   rw [← hl, ← hr, ← zip_unzip xs, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
 
-@[simp] theorem unzip_mkVector {n : Nat} {a : α} {b : β} :
-    unzip (mkVector n (a, b)) = (mkVector n a, mkVector n b) := by
+@[simp] theorem unzip_replicate {a : α} {b : β} {n : Nat} :
+    unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
   ext1 <;> simp
 
+@[deprecated unzip_replicate (since := "2025-03-18")]
+abbrev unzip_mkVector := @unzip_replicate
+
 end Vector

src/Init/GetElem.lean

@@ -135,13 +135,21 @@ theorem getElem_congr_idx [GetElem coll idx elem valid] {c : coll} {i j : idx} {
     (h' : i = j) : c[i] = c[j]'(h' ▸ w) := by
   cases h'; rfl
 
+/--
+Lawful `GetElem?` instances (which extend `GetElem`) are those for which the potentially-failing
+`GetElem?.getElem?` and `GetElem?.getElem!` operators succeed when the validity predicate is
+satisfied, and fail when it is not.
+-/
 class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w))
    (dom : outParam (cont → idx → Prop)) [ge : GetElem? cont idx elem dom] : Prop where
 
+  /-- `GetElem?.getElem?` succeeds when the validity predicate is satisfied and fails otherwise. -/
   getElem?_def (c : cont) (i : idx) [Decidable (dom c i)] :
       c[i]? = if h : dom c i then some (c[i]'h) else none := by
     intros
     try simp only [getElem?] <;> congr
+
+  /-- `GetElem?.getElem!` succeeds and fails when `GetElem.getElem?` succeeds and fails. -/
   getElem!_def [Inhabited elem] (c : cont) (i : idx) :
       c[i]! = match c[i]? with | some e => e | none => default := by
     intros

src/Init/Grind/Tactics.lean

@@ -74,6 +74,11 @@ structure Config where
   using rational numbers, and ignoring divisibility constraints.
   This approach is cheaper but incomplete. -/
   qlia : Bool := false
+  /--
+  If `mbtc` is `true`, `grind` will use model-based theory commbination for creating new case splits.
+  See paper "Model-based Theory Combination" for details.
+  -/
+  mbtc : Bool := true
   deriving Inhabited, BEq
 
 end Lean.Grind

src/Init/Prelude.lean

@@ -483,6 +483,7 @@ inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
 @[match_pattern] protected def HEq.rfl {α : Sort u} {a : α} : HEq a a :=
   HEq.refl a
 
+/-- If two heterogeneously equal terms have the same type, then they are propositionally equal. -/
 theorem eq_of_heq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
   have : (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b :=
     fun _ _ _ _ h₁ =>
@@ -2060,20 +2061,22 @@ instance : LE (BitVec n) where le := (LE.le ·.toNat ·.toNat)
 instance (x y : BitVec n) : Decidable (LE.le x y) :=
   inferInstanceAs (Decidable (LE.le x.toNat y.toNat))
 
-/-- The size of type `UInt8`, that is, `2^8 = 256`. -/
+/-- The number of distinct values representable by `UInt8`, that is, `2^8 = 256`. -/
 abbrev UInt8.size : Nat := 256
 
 /--
-The type of unsigned 8-bit integers. This type has special support in the
-compiler to make it actually 8 bits rather than wrapping a `Nat`.
+Unsigned 8-bit integers.
+
+This type has special support in the compiler so it can be represented by an unboxed 8-bit value
+rather than wrapping a `BitVec 8`.
 -/
 structure UInt8 where
   /--
-  Create a `UInt8` from a `BitVec 8`. This function is overridden with a native implementation.
+  Creates a `UInt8` from a `BitVec 8`. This function is overridden with a native implementation.
   -/
   ofBitVec ::
   /--
-  Unpack a `UInt8` as a `BitVec 8`. This function is overridden with a native implementation.
+  Unpacks a `UInt8` into a `BitVec 8`. This function is overridden with a native implementation.
   -/
   toBitVec : BitVec 8
 
@@ -2081,8 +2084,10 @@ attribute [extern "lean_uint8_of_nat_mk"] UInt8.ofBitVec
 attribute [extern "lean_uint8_to_nat"] UInt8.toBitVec
 
 /--
-Pack a `Nat` less than `2^8` into a `UInt8`.
-This function is overridden with a native implementation.
+Converts a natural number to an 8-bit unsigned integer. Requires a proof that the number is small
+enough to be representable without overflow; it must be smaller than `2^8`.
+
+This function is overridden at runtime with an efficient implementation.
 -/
 @[extern "lean_uint8_of_nat"]
 def UInt8.ofNatLT (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 where
@@ -2090,8 +2095,15 @@ def UInt8.ofNatLT (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 where
 
 set_option bootstrap.genMatcherCode false in
 /--
-Decides equality on `UInt8`.
-This function is overridden with a native implementation.
+Decides whether two 8-bit unsigned integers are equal. Usually accessed via the `DecidableEq UInt8`
+instance.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `UInt8.decEq 123 123 = .isTrue rfl`
+ * `(if (6 : UInt8) = 7 then "yes" else "no") = "no"`
+ * `show (7 : UInt8) = 7 by decide`
 -/
 @[extern "lean_uint8_dec_eq"]
 def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=
@@ -2106,20 +2118,22 @@ instance : DecidableEq UInt8 := UInt8.decEq
 instance : Inhabited UInt8 where
   default := UInt8.ofNatLT 0 (of_decide_eq_true rfl)
 
-/-- The size of type `UInt16`, that is, `2^16 = 65536`. -/
+/-- The number of distinct values representable by `UInt16`, that is, `2^16 = 65536`. -/
 abbrev UInt16.size : Nat := 65536
 
 /--
-The type of unsigned 16-bit integers. This type has special support in the
-compiler to make it actually 16 bits rather than wrapping a `Nat`.
+Unsigned 16-bit integers.
+
+This type has special support in the compiler so it can be represented by an unboxed 16-bit value
+rather than wrapping a `BitVec 16`.
 -/
 structure UInt16 where
   /--
-  Create a `UInt16` from a `BitVec 16`. This function is overridden with a native implementation.
+  Creates a `UInt16` from a `BitVec 16`. This function is overridden with a native implementation.
   -/
   ofBitVec ::
   /--
-  Unpack a `UInt16` as a `BitVec 16`. This function is overridden with a native implementation.
+  Unpacks a `UInt16` into a `BitVec 16`. This function is overridden with a native implementation.
   -/
   toBitVec : BitVec 16
 
@@ -2127,17 +2141,27 @@ attribute [extern "lean_uint16_of_nat_mk"] UInt16.ofBitVec
 attribute [extern "lean_uint16_to_nat"] UInt16.toBitVec
 
 /--
-Pack a `Nat` less than `2^16` into a `UInt16`.
-This function is overridden with a native implementation.
+Converts a natural number to a 16-bit unsigned integer. Requires a proof that the number is small
+enough to be representable without overflow; it must be smaller than `2^16`.
+
+This function is overridden at runtime with an efficient implementation.
 -/
 @[extern "lean_uint16_of_nat"]
 def UInt16.ofNatLT (n : @& Nat) (h : LT.lt n UInt16.size) : UInt16 where
   toBitVec := BitVec.ofNatLT n h
 
 set_option bootstrap.genMatcherCode false in
+
 /--
-Decides equality on `UInt16`.
-This function is overridden with a native implementation.
+Decides whether two 16-bit unsigned integers are equal. Usually accessed via the
+`DecidableEq UInt16` instance.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `UInt16.decEq 123 123 = .isTrue rfl`
+ * `(if (6 : UInt16) = 7 then "yes" else "no") = "no"`
+ * `show (7 : UInt16) = 7 by decide`
 -/
 @[extern "lean_uint16_dec_eq"]
 def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=
@@ -2152,20 +2176,22 @@ instance : DecidableEq UInt16 := UInt16.decEq
 instance : Inhabited UInt16 where
   default := UInt16.ofNatLT 0 (of_decide_eq_true rfl)
 
-/-- The size of type `UInt32`, that is, `2^32 = 4294967296`. -/
+/-- The number of distinct values representable by `UInt32`, that is, `2^32 = 4294967296`. -/
 abbrev UInt32.size : Nat := 4294967296
 
 /--
-The type of unsigned 32-bit integers. This type has special support in the
-compiler to make it actually 32 bits rather than wrapping a `Nat`.
+Unsigned 32-bit integers.
+
+This type has special support in the compiler so it can be represented by an unboxed 32-bit value
+rather than wrapping a `BitVec 32`.
 -/
 structure UInt32 where
   /--
-  Create a `UInt32` from a `BitVec 32`. This function is overridden with a native implementation.
+  Creates a `UInt32` from a `BitVec 32`. This function is overridden with a native implementation.
   -/
   ofBitVec ::
   /--
-  Unpack a `UInt32` as a `BitVec 32`. This function is overridden with a native implementation.
+  Unpacks a `UInt32` into a `BitVec 32`. This function is overridden with a native implementation.
   -/
   toBitVec : BitVec 32
 
@@ -2173,24 +2199,34 @@ attribute [extern "lean_uint32_of_nat_mk"] UInt32.ofBitVec
 attribute [extern "lean_uint32_to_nat"] UInt32.toBitVec
 
 /--
-Pack a `Nat` less than `2^32` into a `UInt32`.
-This function is overridden with a native implementation.
+Converts a natural number to a 32-bit unsigned integer. Requires a proof that the number is small
+enough to be representable without overflow; it must be smaller than `2^32`.
+
+This function is overridden at runtime with an efficient implementation.
 -/
 @[extern "lean_uint32_of_nat"]
 def UInt32.ofNatLT (n : @& Nat) (h : LT.lt n UInt32.size) : UInt32 where
   toBitVec := BitVec.ofNatLT n h
 
 /--
-Unpack a `UInt32` as a `Nat`.
-This function is overridden with a native implementation.
+Converts a 32-bit unsigned integer to an arbitrary-precision natural number.
+
+This function is overridden at runtime with an efficient implementation.
 -/
 @[extern "lean_uint32_to_nat"]
 def UInt32.toNat (n : UInt32) : Nat := n.toBitVec.toNat
 
 set_option bootstrap.genMatcherCode false in
 /--
-Decides equality on `UInt32`.
-This function is overridden with a native implementation.
+Decides whether two 32-bit unsigned integers are equal. Usually accessed via the
+`DecidableEq UInt32` instance.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `UInt32.decEq 123 123 = .isTrue rfl`
+ * `(if (6 : UInt32) = 7 then "yes" else "no") = "no"`
+ * `show (7 : UInt32) = 7 by decide`
 -/
 @[extern "lean_uint32_dec_eq"]
 def UInt32.decEq (a b : UInt32) : Decidable (Eq a b) :=
@@ -2210,16 +2246,31 @@ instance : LE UInt32 where
   le a b := LE.le a.toBitVec b.toBitVec
 
 /--
-Decides less-equal on `UInt32`.
-This function is overridden with a native implementation.
+Decides whether one 8-bit unsigned integer is strictly less than another. Usually accessed via the
+`DecidableLT UInt32` instance.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `(if (6 : UInt32) < 7 then "yes" else "no") = "yes"`
+ * `(if (5 : UInt32) < 5 then "yes" else "no") = "no"`
+ * `show ¬((7 : UInt32) < 7) by decide`
 -/
 @[extern "lean_uint32_dec_lt"]
 def UInt32.decLt (a b : UInt32) : Decidable (LT.lt a b) :=
   inferInstanceAs (Decidable (LT.lt a.toBitVec b.toBitVec))
 
 /--
-Decides less-than on `UInt32`.
-This function is overridden with a native implementation.
+Decides whether one 32-bit signed integer is less than or equal to another. Usually accessed via the
+`DecidableLE UInt32` instance.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `(if (15 : UInt32) ≤ 15 then "yes" else "no") = "yes"`
+ * `(if (15 : UInt32) ≤ 5 then "yes" else "no") = "no"`
+ * `(if (5 : UInt32) ≤ 15 then "yes" else "no") = "yes"`
+ * `show (7 : UInt32) ≤ 7 by decide`
 -/
 @[extern "lean_uint32_dec_le"]
 def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) :=
@@ -2230,37 +2281,50 @@ instance (a b : UInt32) : Decidable (LE.le a b) := UInt32.decLe a b
 instance : Max UInt32 := maxOfLe
 instance : Min UInt32 := minOfLe
 
-/-- The size of type `UInt64`, that is, `2^64 = 18446744073709551616`. -/
+/-- The number of distinct values representable by `UInt64`, that is, `2^64 = 18446744073709551616`. -/
 abbrev UInt64.size : Nat := 18446744073709551616
+
 /--
-The type of unsigned 64-bit integers. This type has special support in the
-compiler to make it actually 64 bits rather than wrapping a `Nat`.
+Unsigned 64-bit integers.
+
+This type has special support in the compiler so it can be represented by an unboxed 64-bit value
+rather than wrapping a `BitVec 64`.
 -/
 structure UInt64 where
   /--
-  Create a `UInt64` from a `BitVec 64`. This function is overridden with a native implementation.
+  Creates a `UInt64` from a `BitVec 64`. This function is overridden with a native implementation.
   -/
   ofBitVec ::
   /--
-  Unpack a `UInt64` as a `BitVec 64`. This function is overridden with a native implementation.
+  Unpacks a `UInt64` into a `BitVec 64`. This function is overridden with a native implementation.
   -/
-  toBitVec: BitVec 64
+  toBitVec : BitVec 64
 
 attribute [extern "lean_uint64_of_nat_mk"] UInt64.ofBitVec
 attribute [extern "lean_uint64_to_nat"] UInt64.toBitVec
 
 /--
-Pack a `Nat` less than `2^64` into a `UInt64`.
-This function is overridden with a native implementation.
+Converts a natural number to a 64-bit unsigned integer. Requires a proof that the number is small
+enough to be representable without overflow; it must be smaller than `2^64`.
+
+This function is overridden at runtime with an efficient implementation.
 -/
 @[extern "lean_uint64_of_nat"]
 def UInt64.ofNatLT (n : @& Nat) (h : LT.lt n UInt64.size) : UInt64 where
   toBitVec := BitVec.ofNatLT n h
 
 set_option bootstrap.genMatcherCode false in
+
 /--
-Decides equality on `UInt64`.
-This function is overridden with a native implementation.
+Decides whether two 64-bit unsigned integers are equal. Usually accessed via the
+`DecidableEq UInt64` instance.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `UInt64.decEq 123 123 = .isTrue rfl`
+ * `(if (6 : UInt64) = 7 then "yes" else "no") = "no"`
+ * `show (7 : UInt64) = 7 by decide`
 -/
 @[extern "lean_uint64_dec_eq"]
 def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
@@ -2275,7 +2339,7 @@ instance : DecidableEq UInt64 := UInt64.decEq
 instance : Inhabited UInt64 where
   default := UInt64.ofNatLT 0 (of_decide_eq_true rfl)
 
-/-- The size of type `USize`, that is, `2^System.Platform.numBits`. -/
+/-- The number of distinct values representable by `USize`, that is, `2^System.Platform.numBits`. -/
 abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
 
 theorem USize.size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
@@ -2290,20 +2354,19 @@ theorem USize.size_pos : LT.lt 0 USize.size :=
   | _, Or.inr rfl => of_decide_eq_true rfl
 
 /--
-A `USize` is an unsigned integer with the size of a word
-for the platform's architecture.
+Unsigned integers that are the size of a word on the platform's architecture.
 
-For example, if running on a 32-bit machine, USize is equivalent to UInt32.
-Or on a 64-bit machine, UInt64.
+On a 32-bit architecture, `USize` is equivalent to `UInt32`. On a 64-bit machine, it is equivalent
+to `UInt64`.
 -/
 structure USize where
   /--
-  Create a `USize` from a `BitVec System.Platform.numBits`. This function is overridden with a
+  Creates a `USize` from a `BitVec System.Platform.numBits`. This function is overridden with a
   native implementation.
   -/
   ofBitVec ::
   /--
-  Unpack a `USize` as a `BitVec System.Platform.numBits`. This function is overridden with a native
+  Unpacks a `USize` into a `BitVec System.Platform.numBits`. This function is overridden with a native
   implementation.
   -/
   toBitVec : BitVec System.Platform.numBits
@@ -2312,8 +2375,10 @@ attribute [extern "lean_usize_of_nat_mk"] USize.ofBitVec
 attribute [extern "lean_usize_to_nat"] USize.toBitVec
 
 /--
-Pack a `Nat` less than `USize.size` into a `USize`.
-This function is overridden with a native implementation.
+Converts a natural number to a `USize`. Requires a proof that the number is small enough to be
+representable without overflow.
+
+This function is overridden at runtime with an efficient implementation.
 -/
 @[extern "lean_usize_of_nat"]
 def USize.ofNatLT (n : @& Nat) (h : LT.lt n USize.size) : USize where
@@ -2321,8 +2386,15 @@ def USize.ofNatLT (n : @& Nat) (h : LT.lt n USize.size) : USize where
 
 set_option bootstrap.genMatcherCode false in
 /--
-Decides equality on `USize`.
-This function is overridden with a native implementation.
+Decides whether two word-sized unsigned integers are equal. Usually accessed via the
+`DecidableEq USize` instance.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `USize.decEq 123 123 = .isTrue rfl`
+ * `(if (6 : USize) = 7 then "yes" else "no") = "no"`
+ * `show (7 : USize) = 7 by decide`
 -/
 @[extern "lean_usize_dec_eq"]
 def USize.decEq (a b : USize) : Decidable (Eq a b) :=

src/Init/System/IO.lean

@@ -1573,6 +1573,10 @@ end CancelToken
 namespace FS
 namespace Stream
 
+/--
+Creates a Lean stream from a file handle. Each stream operation is implemented by the corresponding
+file handle operation.
+-/
 @[export lean_stream_of_handle]
 def ofHandle (h : Handle) : Stream where
   flush   := Handle.flush h

src/Init/System/ST.lean

@@ -122,6 +122,9 @@ end Prim
 section
 variable {σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST σ) m]
 
+/--
+Creates a new mutable reference that contains the provided value `a`.
+-/
 @[inline] def mkRef {α : Type} (a : α) : m (Ref σ α) :=  liftM <| Prim.mkRef a
 /--
 Reads the value of a mutable reference.

src/Init/WF.lean

@@ -52,10 +52,22 @@ a well founded relation, then the function terminates.
 Well-founded relations are sometimes called _Artinian_ or said to satisfy the “descending chain condition”.
 -/
 inductive WellFounded {α : Sort u} (r : α → α → Prop) : Prop where
+  /--
+  If all elements are accessible via `r`, then `r` is well-founded.
+  -/
   | intro (h : ∀ a, Acc r a) : WellFounded r
 
+/--
+A type that has a standard well-founded relation.
+
+Instances are used to prove that functions terminate using well-founded recursion by showing that
+recursive calls reduce some measure according to a well-founded relation. This relation can combine
+well-founded relations on the recursive function's parameters.
+-/
 class WellFoundedRelation (α : Sort u) where
+  /-- A well-founded relation on `α`. -/
   rel : α → α → Prop
+  /-- A proof that `rel` is, in fact, well-founded. -/
   wf  : WellFounded rel
 
 namespace WellFounded
@@ -88,6 +100,13 @@ end
 
 variable {α : Sort u} {C : α → Sort v} {r : α → α → Prop}
 
+/--
+A well-founded fixpoint. If satisfying the motive `C` for all values that are smaller according to a
+well-founded relation allows it to be satisfied for the current value, then it is satisfied for all
+values.
+
+This function is used as part of the elaboration of well-founded recursion.
+-/
 -- Well-founded fixpoint
 noncomputable def fix (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x :=
   fixF F x (apply hwf x)
@@ -145,6 +164,9 @@ theorem wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
   ⟨fun a => accessible f (apply h (f a))⟩
 end InvImage
 
+/--
+The inverse image of a well-founded relation is well-founded.
+-/
 @[reducible] def invImage (f : α → β) (h : WellFoundedRelation β) : WellFoundedRelation α where
   rel := InvImage h.rel f
   wf  := InvImage.wf f h.wf

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddharth Bhat
 -/
 prelude
-import Lean.Data.HashMap
 import Lean.Runtime
 import Lean.Compiler.NameMangling
 import Lean.Compiler.ExportAttr

src/Lean/Compiler/IR/ExpandResetReuse.lean

@@ -85,7 +85,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
 /-- Try to erase `inc` instructions on projections of `y` occurring in the tail of `bs`.
    Return the updated `bs` and a bit mask specifying which `inc`s have been removed. -/
 def eraseProjIncFor (n : Nat) (y : VarId) (bs : Array FnBody) : Array FnBody × Mask :=
-  eraseProjIncForAux y bs (mkArray n none) #[]
+  eraseProjIncForAux y bs (.replicate n none) #[]
 
 /-- Replace `reuse x ctor ...` with `ctor ...`, and remove `dec x` -/
 partial def reuseToCtor (x : VarId) : FnBody → FnBody

src/Lean/Compiler/LCNF/FixedParams.lean

@@ -169,7 +169,7 @@ def mkFixedParamsMap (decls : Array Decl) : NameMap (Array Bool) := Id.run do
   for decl in decls do
     let values := mkInitialValues decl.params.size
     let assignment := mkAssignment decl values
-    let fixed := Array.mkArray decl.params.size true
+    let fixed := Array.replicate decl.params.size true
     match decl.value with
     | .code c =>
       match evalCode c |>.run { main := decl, decls, assignment } |>.run { fixed } with

src/Lean/Compiler/LCNF/Simp/DiscrM.lean

@@ -98,7 +98,7 @@ where
       return { ctx with discrCtorMap := ctx.discrCtorMap.insert discr ctorInfo, ctorDiscrMap := ctx.ctorDiscrMap.insert ctor.toExpr discr }
     else
       -- For the discrCtor map, the constructor parameters are irrelevant for optimizations that use this information
-      let ctorInfo := .ctor ctorVal (mkArray ctorVal.numParams Arg.erased ++ fieldArgs)
+      let ctorInfo := .ctor ctorVal (.replicate ctorVal.numParams Arg.erased ++ fieldArgs)
       return { ctx with discrCtorMap := ctx.discrCtorMap.insert discr ctorInfo }
 
 @[inline, inherit_doc withDiscrCtorImp] def withDiscrCtor [MonadFunctorT DiscrM m] (discr : FVarId) (ctorName : Name) (ctorFields : Array Param) : m α → m α :=

src/Lean/Compiler/LCNF/SpecInfo.lean

@@ -148,7 +148,7 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do
   let mut declsInfo := #[]
   for decl in decls do
     if hasNospecializeAttribute (← getEnv) decl.name then
-      declsInfo := declsInfo.push (mkArray decl.params.size .other)
+      declsInfo := declsInfo.push (.replicate decl.params.size .other)
     else
       let specArgs? := getSpecializationArgs? (← getEnv) decl.name
       let contains (i : Nat) : Bool := specArgs?.getD #[] |>.contains i

src/Lean/CoreM.lean

@@ -130,6 +130,8 @@ structure Context where
   errors; see also `logMessage` below.
   -/
   suppressElabErrors : Bool := false
+  /-- Cache of `Lean.inheritedTraceOptions`. -/
+  inheritedTraceOptions : Std.HashSet Name := {}
   deriving Nonempty
 
 /-- CoreM is a monad for manipulating the Lean environment.
@@ -175,9 +177,11 @@ instance : MonadWithOptions CoreM where
           maxRecDepth := maxRecDepth.get options })
       x
 
--- Helper function for ensuring fields that depend on `options` have the correct value.
+-- Helper function for ensuring fields derived from e.g. options have the correct value.
 @[inline] private def withConsistentCtx (x : CoreM α) : CoreM α := do
-  withOptions id x
+  let inheritedTraceOptions ← inheritedTraceOptions.get
+  withReader (fun ctx => { ctx with inheritedTraceOptions }) do
+    withOptions id x
 
 instance : AddMessageContext CoreM where
   addMessageContext := addMessageContextPartial
@@ -246,6 +250,7 @@ instance : MonadLift IO CoreM where
 instance : MonadTrace CoreM where
   getTraceState := return (← get).traceState
   modifyTraceState f := modify fun s => { s with traceState := f s.traceState }
+  getInheritedTraceOptions := return (← read).inheritedTraceOptions
 
 structure SavedState extends State where
   /-- Number of heartbeats passed inside `withRestoreOrSaveFull`, not used otherwise. -/

src/Lean/Data.lean

@@ -6,8 +6,6 @@ Authors: Sebastian Ullrich
 prelude
 import Lean.Data.AssocList
 import Lean.Data.Format
-import Lean.Data.HashMap
-import Lean.Data.HashSet
 import Lean.Data.Json
 import Lean.Data.JsonRpc
 import Lean.Data.KVMap

src/Lean/Data/Array.lean

@@ -34,7 +34,7 @@ Example:
 -/
 def filterPairsM {m} [Monad m] {α} (a : Array α) (f : α → α → m (Bool × Bool)) :
     m (Array α) := do
-  let mut removed := Array.mkArray a.size false
+  let mut removed := Array.replicate a.size false
   let mut numRemoved := 0
   for h1 : i in [:a.size] do for h2 : j in [i+1:a.size] do
     unless removed[i]! || removed[j]! do

src/Lean/Data/FuzzyMatching.lean

@@ -99,11 +99,11 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
   between the substrings pattern[:i+1] and word[:j+1] assuming that pattern[i] misses at word[j] (k = 0, i.e.
   it was matched earlier), or matches at word[j] (k = 1). A value of `none` corresponds to a score of -∞, and is used
   where no such match/miss is possible or for unneeded parts of the table. -/
-  let mut result : Array (Option Int) := Array.mkArray (pattern.length * word.length * 2) none
-  let mut runLengths : Array Int := Array.mkArray (pattern.length * word.length) 0
+  let mut result : Array (Option Int) := Array.replicate (pattern.length * word.length * 2) none
+  let mut runLengths : Array Int := Array.replicate (pattern.length * word.length) 0
 
   -- penalty for starting a consecutive run at each index
-  let mut startPenalties : Array Int := Array.mkArray word.length 0
+  let mut startPenalties : Array Int := Array.replicate word.length 0
 
   let mut lastSepIdx := 0
   let mut penaltyNs : Int := 0

src/Lean/Data/HashMap.lean

@@ -1,292 +0,0 @@
-/-
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
--/
-prelude
-import Init.Data.Nat.Power2
-import Lean.Data.AssocList
-import Std.Data.HashMap.Basic
-import Std.Data.HashMap.Raw
-namespace Lean
-
-def HashMapBucket (α : Type u) (β : Type v) :=
-  { b : Array (AssocList α β) // b.size.isPowerOfTwo }
-
-def HashMapBucket.update {α : Type u} {β : Type v} (data : HashMapBucket α β) (i : USize) (d : AssocList α β) (h : i.toNat < data.val.size) : HashMapBucket α β :=
-  ⟨ data.val.uset i d h,
-    by erw [Array.size_set]; apply data.property ⟩
-
-@[simp] theorem HashMapBucket.size_update {α : Type u} {β : Type v} (data : HashMapBucket α β) (i : USize) (d : AssocList α β)
-    (h : i.toNat < data.val.size) : (data.update i d h).val.size = data.val.size := by
-  simp [update, Array.uset]
-
-structure HashMapImp (α : Type u) (β : Type v) where
-  size       : Nat
-  buckets    : HashMapBucket α β
-
-private def numBucketsForCapacity (capacity : Nat) : Nat :=
-  -- a "load factor" of 0.75 is the usual standard for hash maps
-  capacity * 4 / 3
-
-def mkHashMapImp {α : Type u} {β : Type v} (capacity := 8) : HashMapImp α β :=
-  { size       := 0
-    buckets    :=
-    ⟨mkArray (numBucketsForCapacity capacity).nextPowerOfTwo AssocList.nil,
-     by simp; apply Nat.isPowerOfTwo_nextPowerOfTwo⟩ }
-
-namespace HashMapImp
-variable {α : Type u} {β : Type v}
-
-/- Remark: we use a C implementation because this function is performance critical. -/
-@[extern "lean_hashmap_mk_idx"]
-private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize // u.toNat < sz } :=
-  -- TODO: avoid `if` in the reference implementation
-  let u := hash.toUSize &&& (sz.toUSize - 1)
-  if h' : u.toNat < sz then
-    ⟨u, h'⟩
-  else
-    ⟨0, by simp; apply Nat.pos_of_isPowerOfTwo h⟩
-
-@[inline] def reinsertAux (hashFn : α → UInt64) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β :=
-  let ⟨i, h⟩ := mkIdx (hashFn a) data.property
-  data.update i (AssocList.cons a b data.val[i]) h
-
-@[inline] def foldBucketsM {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashMapBucket α β) (d : δ) (f : δ → α → β → m δ) : m δ :=
-  data.val.foldlM (init := d) fun d b => b.foldlM f d
-
-@[inline] def foldBuckets {δ : Type w} (data : HashMapBucket α β) (d : δ) (f : δ → α → β → δ) : δ :=
-  Id.run $ foldBucketsM data d f
-
-@[inline] def foldM {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → β → m δ) (d : δ) (h : HashMapImp α β) : m δ :=
-  foldBucketsM h.buckets d f
-
-@[inline] def fold {δ : Type w} (f : δ → α → β → δ) (d : δ) (m : HashMapImp α β) : δ :=
-  foldBuckets m.buckets d f
-
-@[inline] def forBucketsM {m : Type w → Type w} [Monad m] (data : HashMapBucket α β) (f : α → β → m PUnit) : m PUnit :=
-  data.val.forM fun b => b.forM f
-
-@[inline] def forM {m : Type w → Type w} [Monad m] (f : α → β → m PUnit) (h : HashMapImp α β) : m PUnit :=
-  forBucketsM h.buckets f
-
-def findEntry? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
-  match m with
-  | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    buckets.val[i].findEntry? a
-
-def find? [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β :=
-  match m with
-  | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    buckets.val[i].find? a
-
-def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
-  match m with
-  | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    buckets.val[i].contains a
-
-def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (target : HashMapBucket α β) : HashMapBucket α β :=
-  if h : i < source.size then
-     let es  : AssocList α β   := source[i]
-     -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
-     let source                := source.set i AssocList.nil
-     let target                := es.foldl (reinsertAux hash) target
-     moveEntries (i+1) source target
-  else target
-termination_by source.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
-  let bucketsNew : HashMapBucket α β := ⟨
-    mkArray (buckets.val.size * 2) AssocList.nil,
-    by simp; apply Nat.mul2_isPowerOfTwo_of_isPowerOfTwo buckets.property
-  ⟩
-  { size    := size,
-    buckets := moveEntries 0 buckets.val bucketsNew }
-
-@[inline] def insert [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β × Bool :=
-  match m with
-  | ⟨size, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    let bkt    := buckets.val[i]
-    if bkt.contains a then
-      -- make sure `bkt` is used linearly in the following call to `replace`
-      let buckets' := buckets.update i .nil h
-      (⟨size, buckets'.update i (bkt.replace a b) (by simpa [buckets'])⟩, true)
-    else
-      let size'    := size + 1
-      let buckets' := buckets.update i (AssocList.cons a b bkt) h
-      if numBucketsForCapacity size' ≤ buckets.val.size then
-        ({ size := size', buckets := buckets' }, false)
-      else
-        (expand size' buckets', false)
-
-@[inline] def insertIfNew [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β × Option β :=
-  match m with
-  | ⟨size, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    let bkt    := buckets.val[i]
-    if let some b := bkt.find? a then
-      (⟨size, buckets⟩, some b)
-    else
-      let size'    := size + 1
-      let buckets' := buckets.update i (AssocList.cons a b bkt) h
-      if numBucketsForCapacity size' ≤ buckets.val.size then
-        ({ size := size', buckets := buckets' }, none)
-      else
-        (expand size' buckets', none)
-
-
-def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
-  match m with
-  | ⟨ size, buckets ⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    let bkt    := buckets.val[i]
-    if bkt.contains a then
-      -- make sure `bkt` is used linearly in the following call to `erase`
-      let buckets' := buckets.update i .nil h
-      ⟨size - 1, buckets'.update i (bkt.erase a) (by simpa [buckets'])⟩
-    else
-      ⟨size, buckets⟩
-
-inductive WellFormed [BEq α] [Hashable α] : HashMapImp α β → Prop where
-  | mkWff          : ∀ n,                    WellFormed (mkHashMapImp n)
-  | insertWff      : ∀ m a b, WellFormed m → WellFormed (insert m a b |>.1)
-  | insertIfNewWff : ∀ m a b, WellFormed m → WellFormed (insertIfNew m a b |>.1)
-  | eraseWff       : ∀ m a,   WellFormed m → WellFormed (erase m a)
-
-end HashMapImp
-
-def HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :=
-  { m : HashMapImp α β // m.WellFormed }
-
-open Lean.HashMapImp
-
-def mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (capacity := 8) : HashMap α β :=
-  ⟨ mkHashMapImp capacity, WellFormed.mkWff capacity ⟩
-
-namespace HashMap
-instance [BEq α] [Hashable α] : Inhabited (HashMap α β) where
-  default := mkHashMap
-
-instance [BEq α] [Hashable α] : EmptyCollection (HashMap α β) := ⟨mkHashMap⟩
-
-@[inline] def empty [BEq α] [Hashable α] : HashMap α β :=
-  mkHashMap
-
-variable {α : Type u} {β : Type v} {_ : BEq α} {_ : Hashable α}
-
-def insert (m : HashMap α β) (a : α) (b : β) : HashMap α β :=
-  match m with
-  | ⟨ m, hw ⟩ =>
-    match h:m.insert a b with
-    | (m', _) => ⟨ m', by have aux := WellFormed.insertWff m a b hw; rw [h] at aux; assumption ⟩
-
-/-- Similar to `insert`, but also returns a Boolean flag indicating whether an existing entry has been replaced with `a -> b`. -/
-def insert' (m : HashMap α β) (a : α) (b : β) : HashMap α β × Bool :=
-  match m with
-  | ⟨ m, hw ⟩ =>
-    match h:m.insert a b with
-    | (m', replaced) => (⟨ m', by have aux := WellFormed.insertWff m a b hw; rw [h] at aux; assumption ⟩, replaced)
-
-/--
-Similar to `insert`, but returns `some old` if the map already had an entry `α → old`.
-If the result is `some old`, the resulting map is equal to `m`. -/
-def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option β :=
-  match m with
-  | ⟨ m, hw ⟩ =>
-    match h:m.insertIfNew a b with
-    | (m', old) => (⟨ m', by have aux := WellFormed.insertIfNewWff m a b hw; rw [h] at aux; assumption ⟩, old)
-
-@[inline] def erase (m : HashMap α β) (a : α) : HashMap α β :=
-  match m with
-  | ⟨ m, hw ⟩ => ⟨ m.erase a, WellFormed.eraseWff m a hw ⟩
-
-@[inline] def findEntry? (m : HashMap α β) (a : α) : Option (α × β) :=
-  match m with
-  | ⟨ m, _ ⟩ => m.findEntry? a
-
-@[inline] def find? (m : HashMap α β) (a : α) : Option β :=
-  match m with
-  | ⟨ m, _ ⟩ => m.find? a
-
-@[inline] def findD (m : HashMap α β) (a : α) (b₀ : β) : β :=
-  (m.find? a).getD b₀
-
-@[inline] def find! [Inhabited β] (m : HashMap α β) (a : α) : β :=
-  match m.find? a with
-  | some b => b
-  | none   => panic! "key is not in the map"
-
-instance : GetElem (HashMap α β) α (Option β) fun _ _ => True where
-  getElem m k _ := m.find? k
-
-@[inline] def contains (m : HashMap α β) (a : α) : Bool :=
-  match m with
-  | ⟨ m, _ ⟩ => m.contains a
-
-@[inline] def foldM {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → β → m δ) (init : δ) (h : HashMap α β) : m δ :=
-  match h with
-  | ⟨ h, _ ⟩ => h.foldM f init
-
-@[inline] def fold {δ : Type w} (f : δ → α → β → δ) (init : δ) (m : HashMap α β) : δ :=
-  match m with
-  | ⟨ m, _ ⟩ => m.fold f init
-
-@[inline] def forM {m : Type w → Type w} [Monad m] (f : α → β → m PUnit) (h : HashMap α β) : m PUnit :=
-  match h with
-  | ⟨ h, _ ⟩ => h.forM f
-
-@[inline] def size (m : HashMap α β) : Nat :=
-  match m with
-  | ⟨ {size := sz, ..}, _ ⟩ => sz
-
-@[inline] def isEmpty (m : HashMap α β) : Bool :=
-  m.size = 0
-
-def toList (m : HashMap α β) : List (α × β) :=
-  m.fold (init := []) fun r k v => (k, v)::r
-
-def toArray (m : HashMap α β) : Array (α × β) :=
-  m.fold (init := #[]) fun r k v => r.push (k, v)
-
-def numBuckets (m : HashMap α β) : Nat :=
-  m.val.buckets.val.size
-
-variable [BEq α] [Hashable α]
-
-/-- Builds a `HashMap` from a list of key-value pairs. Values of duplicated keys are replaced by their respective last occurrences. -/
-def ofList (l : List (α × β)) : HashMap α β :=
-  l.foldl (init := HashMap.empty) (fun m p => m.insert p.fst p.snd)
-
-/-- Variant of `ofList` which accepts a function that combines values of duplicated keys. -/
-def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β :=
-  l.foldl (init := HashMap.empty)
-    (fun m p =>
-      match m.find? p.fst with
-        | none   => m.insert p.fst p.snd
-        | some v => m.insert p.fst $ f v p.snd)
-
-attribute [deprecated Std.HashMap.insert (since := "2024-08-08")] HashMap.insert
-attribute [deprecated Std.HashMap.containsThenInsert (since := "2024-08-08")] HashMap.insert'
-attribute [deprecated Std.HashMap.insertIfNew (since := "2024-08-08")] HashMap.insertIfNew
-attribute [deprecated Std.HashMap.erase (since := "2024-08-08")] HashMap.erase
-attribute [deprecated "Use `m[k]?` instead." (since := "2024-08-08")] HashMap.findEntry?
-attribute [deprecated "Use `m[k]?` instead." (since := "2024-08-08")] HashMap.find?
-attribute [deprecated "Use `m[k]?.getD` instead." (since := "2024-08-08")] HashMap.findD
-attribute [deprecated "Use `m[k]!` instead." (since := "2024-08-08")] HashMap.find!
-attribute [deprecated Std.HashMap.contains (since := "2024-08-08")] HashMap.contains
-attribute [deprecated Std.HashMap.foldM (since := "2024-08-08")] HashMap.foldM
-attribute [deprecated Std.HashMap.fold (since := "2024-08-08")] HashMap.fold
-attribute [deprecated Std.HashMap.forM (since := "2024-08-08")] HashMap.forM
-attribute [deprecated Std.HashMap.size (since := "2024-08-08")] HashMap.size
-attribute [deprecated Std.HashMap.isEmpty (since := "2024-08-08")] HashMap.isEmpty
-attribute [deprecated Std.HashMap.toList (since := "2024-08-08")] HashMap.toList
-attribute [deprecated Std.HashMap.toArray (since := "2024-08-08")] HashMap.toArray
-attribute [deprecated "Deprecateed without a replacement." (since := "2024-08-08")] HashMap.numBuckets
-attribute [deprecated "Deprecateed without a replacement." (since := "2024-08-08")] HashMap.ofListWith
-
-end Lean.HashMap

src/Lean/Data/HashSet.lean

@@ -1,225 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
--/
-prelude
-import Init.Data.Nat.Power2
-import Std.Data.HashSet.Basic
-import Std.Data.HashSet.Raw
-namespace Lean
-universe u v w
-
-def HashSetBucket (α : Type u) :=
-  { b : Array (List α) // b.size.isPowerOfTwo }
-
-def HashSetBucket.update {α : Type u} (data : HashSetBucket α) (i : USize) (d : List α) (h : i.toNat < data.val.size) : HashSetBucket α :=
-  ⟨ data.val.uset i d h,
-    by erw [Array.size_set]; apply data.property ⟩
-
-@[simp] theorem HashSetBucket.size_update {α : Type u} (data : HashSetBucket α) (i : USize) (d : List α) (h : i.toNat < data.val.size) :
-    (data.update i d h).val.size = data.val.size := by
-  simp [update, Array.uset]
-
-structure HashSetImp (α : Type u) where
-  size       : Nat
-  buckets    : HashSetBucket α
-
-def mkHashSetImp {α : Type u} (capacity := 8) : HashSetImp α :=
-  { size       := 0
-    buckets    :=
-    ⟨mkArray ((capacity * 4) / 3).nextPowerOfTwo [],
-     by simp; apply Nat.isPowerOfTwo_nextPowerOfTwo⟩ }
-
-namespace HashSetImp
-variable {α : Type u}
-
-/- Remark: we use a C implementation because this function is performance critical. -/
-@[extern "lean_hashset_mk_idx"]
-private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize // u.toNat < sz } :=
-  -- TODO: avoid `if` in the reference implementation
-  let u := hash.toUSize &&& (sz.toUSize - 1)
-  if h' : u.toNat < sz then
-    ⟨u, h'⟩
-  else
-    ⟨0, by simp; apply Nat.pos_of_isPowerOfTwo h⟩
-
-@[inline] def reinsertAux (hashFn : α → UInt64) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
-  let ⟨i, h⟩ := mkIdx (hashFn a) data.property
-  data.update i (a :: data.val[i]) h
-
-@[inline] def foldBucketsM {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashSetBucket α) (d : δ) (f : δ → α → m δ) : m δ :=
-  data.val.foldlM (init := d) fun d as => as.foldlM f d
-
-@[inline] def foldBuckets {δ : Type w} (data : HashSetBucket α) (d : δ) (f : δ → α → δ) : δ :=
-  Id.run $ foldBucketsM data d f
-
-@[inline] def foldM {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → m δ) (d : δ) (h : HashSetImp α) : m δ :=
-  foldBucketsM h.buckets d f
-
-@[inline] def fold {δ : Type w} (f : δ → α → δ) (d : δ) (m : HashSetImp α) : δ :=
-  foldBuckets m.buckets d f
-
-@[inline] def forBucketsM {m : Type w → Type w} [Monad m] (data : HashSetBucket α) (f : α → m PUnit) : m PUnit :=
-  data.val.forM fun as => as.forM f
-
-@[inline] def forM {m : Type w → Type w} [Monad m] (f : α → m PUnit) (h : HashSetImp α) : m PUnit :=
-  forBucketsM h.buckets f
-
-def find? [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α :=
-  match m with
-  | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    buckets.val[i].find? (fun a' => a == a')
-
-def contains [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
-  match m with
-  | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    buckets.val[i].contains a
-
-def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : HashSetBucket α) : HashSetBucket α :=
-  if h : i < source.size then
-     let es  : List α   := source[i]
-     -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
-     let source                := source.set i []
-     let target                := es.foldl (reinsertAux hash) target
-     moveEntries (i+1) source target
-  else
-    target
-termination_by source.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
-  let bucketsNew : HashSetBucket α := ⟨
-    mkArray (buckets.val.size * 2) [],
-    by simp; apply Nat.mul2_isPowerOfTwo_of_isPowerOfTwo buckets.property
-  ⟩
-  { size    := size,
-    buckets := moveEntries 0 buckets.val bucketsNew }
-
-def insert [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
-  match m with
-  | ⟨size, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    let bkt    := buckets.val[i]
-    if bkt.contains a
-    then
-      -- make sure `bkt` is used linearly in the following call to `replace`
-      let buckets' := buckets.update i .nil h
-      ⟨size, buckets'.update i (bkt.replace a a) (by simpa [buckets'])⟩
-    else
-      let size'    := size + 1
-      let buckets' := buckets.update i (a :: bkt) h
-      if size' ≤ buckets.val.size
-      then { size := size', buckets := buckets' }
-      else expand size' buckets'
-
-def erase [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
-  match m with
-  | ⟨ size, buckets ⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    let bkt    := buckets.val[i]
-    if bkt.contains a then
-      -- make sure `bkt` is used linearly in the following call to `erase`
-      let buckets' := buckets.update i .nil h
-      ⟨size - 1, buckets'.update i (bkt.erase a) (by simpa [buckets'])⟩
-    else
-      ⟨size, buckets⟩
-
-inductive WellFormed [BEq α] [Hashable α] : HashSetImp α → Prop where
-  | mkWff     : ∀ n,                  WellFormed (mkHashSetImp n)
-  | insertWff : ∀ m a, WellFormed m → WellFormed (insert m a)
-  | eraseWff  : ∀ m a, WellFormed m → WellFormed (erase m a)
-
-end HashSetImp
-
-def HashSet (α : Type u) [BEq α] [Hashable α] :=
-  { m : HashSetImp α // m.WellFormed }
-
-open HashSetImp
-
-def mkHashSet {α : Type u} [BEq α] [Hashable α] (capacity := 8) : HashSet α :=
-  ⟨ mkHashSetImp capacity, WellFormed.mkWff capacity ⟩
-
-namespace HashSet
-@[inline] def empty [BEq α] [Hashable α] : HashSet α :=
-  mkHashSet
-
-instance [BEq α] [Hashable α] : Inhabited (HashSet α) where
-  default := mkHashSet
-
-instance [BEq α] [Hashable α] : EmptyCollection (HashSet α) := ⟨mkHashSet⟩
-
-variable {α : Type u} {_ : BEq α} {_ : Hashable α}
-
-@[inline] def insert (m : HashSet α) (a : α) : HashSet α :=
-  match m with
-  | ⟨ m, hw ⟩ => ⟨ m.insert a, WellFormed.insertWff m a hw ⟩
-
-@[inline] def erase (m : HashSet α) (a : α) : HashSet α :=
-  match m with
-  | ⟨ m, hw ⟩ => ⟨ m.erase a, WellFormed.eraseWff m a hw ⟩
-
-@[inline] def find? (m : HashSet α) (a : α) : Option α :=
-  match m with
-  | ⟨ m, _ ⟩ => m.find? a
-
-@[inline] def contains (m : HashSet α) (a : α) : Bool :=
-  match m with
-  | ⟨ m, _ ⟩ => m.contains a
-
-@[inline] def foldM {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → m δ) (init : δ) (h : HashSet α) : m δ :=
-  match h with
-  | ⟨ h, _ ⟩ => h.foldM f init
-
-@[inline] def fold {δ : Type w} (f : δ → α → δ) (init : δ) (m : HashSet α) : δ :=
-  match m with
-  | ⟨ m, _ ⟩ => m.fold f init
-
-@[inline] def forM {m : Type w → Type w} [Monad m] (h : HashSet α) (f : α → m PUnit) : m PUnit :=
-  match h with
-  | ⟨h, _⟩ => h.forM f
-
-instance : ForM m (HashSet α) α where
-  forM := HashSet.forM
-
-instance : ForIn m (HashSet α) α where
-  forIn := ForM.forIn
-
-@[inline] def size (m : HashSet α) : Nat :=
-  match m with
-  | ⟨ {size := sz, ..}, _ ⟩ => sz
-
-@[inline] def isEmpty (m : HashSet α) : Bool :=
-  m.size = 0
-
-def toList (m : HashSet α) : List α :=
-  m.fold (init := []) fun r a => a::r
-
-def toArray (m : HashSet α) : Array α :=
-  m.fold (init := #[]) fun r a => r.push a
-
-def numBuckets (m : HashSet α) : Nat :=
-  m.val.buckets.val.size
-
-/-- Insert many elements into a HashSet. -/
-def insertMany [ForIn Id ρ α] (s : HashSet α) (as : ρ) : HashSet α := Id.run do
-  let mut s := s
-  for a in as do
-    s := s.insert a
-  return s
-
-/--
-`O(|t|)` amortized. Merge two `HashSet`s.
--/
-@[inline]
-def merge {α : Type u} [BEq α] [Hashable α] (s t : HashSet α) : HashSet α :=
-  t.fold (init := s) fun s a => s.insert a
-  -- We don't use `insertMany` here because it gives weird universes.
-
-attribute [deprecated Std.HashSet (since := "2024-08-08")] HashSet
-attribute [deprecated Std.HashSet.Raw (since := "2024-08-08")] HashSetImp
-attribute [deprecated Std.HashSet.Raw.empty (since := "2024-08-08")] mkHashSetImp
-attribute [deprecated Std.HashSet.empty (since := "2024-08-08")] mkHashSet
-attribute [deprecated Std.HashSet.empty (since := "2024-08-08")] HashSet.empty

src/Lean/Data/NameMap.lean

@@ -5,7 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import Std.Data.HashSet.Basic
-import Lean.Data.HashSet
 import Lean.Data.RBMap
 import Lean.Data.RBTree
 import Lean.Data.SSet

src/Lean/Data/PersistentHashMap.lean

@@ -39,7 +39,7 @@ abbrev maxDepth      : USize  := 7
 abbrev maxCollisions : Nat    := 4
 
 def mkEmptyEntriesArray {α β} : Array (Entry α β (Node α β)) :=
-  (Array.mkArray PersistentHashMap.branching.toNat PersistentHashMap.Entry.null)
+  (Array.replicate PersistentHashMap.branching.toNat PersistentHashMap.Entry.null)
 
 end PersistentHashMap
 

src/Lean/Data/SMap.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Std.Data.HashMap.Basic
-import Lean.Data.HashMap
 import Lean.Data.PersistentHashMap
 universe u v w w'
 

src/Lean/Elab/Binders.lean

@@ -94,9 +94,14 @@ partial def quoteAutoTactic : Syntax → CoreM Expr
   | .atom _ val => return .app (.const ``mkAtom []) (toExpr val)
   | .missing    => throwError "invalid auto tactic, tactic is missing"
 
-def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
+/--
+Adds a declaration whose value is a Syntax expression representing `tactic`.
+If `name?` is provided, it is used for the declaration name, and otherwise a fresh name is generated.
+Returns the declaration name.
+-/
+def declareTacticSyntax (tactic : Syntax) (name? : Option Name := none) : TermElabM Name :=
   withFreshMacroScope do
-    let name ← MonadQuotation.addMacroScope ((← getEnv).asyncPrefix?.getD .anonymous ++ `_auto)
+    let name ← name?.getDM do MonadQuotation.addMacroScope ((← getEnv).asyncPrefix?.getD .anonymous ++ `_auto)
     let type := Lean.mkConst `Lean.Syntax
     let value ← quoteAutoTactic tactic
     trace[Elab.autoParam] value

src/Lean/Elab/ComputedFields.lean

@@ -58,7 +58,7 @@ abbrev M := ReaderT Context MetaM
 def getComputedFieldValue (computedField : Name) (ctorTerm : Expr) : MetaM Expr := do
   let ctorName := ctorTerm.getAppFn.constName!
   let ind ← getConstInfoInduct (← getConstInfoCtor ctorName).induct
-  let val ← mkAppOptM computedField (mkArray (ind.numParams+ind.numIndices) none ++ #[some ctorTerm])
+  let val ← mkAppOptM computedField (.replicate (ind.numParams+ind.numIndices) none ++ #[some ctorTerm])
   let val ←
     if let some wfEqn := WF.eqnInfoExt.find? (← getEnv) computedField then
       pure <| mkAppN (wfEqn.value.instantiateLevelParams wfEqn.levelParams val.getAppFn.constLevels!) val.getAppArgs

src/Lean/Elab/MutualInductive.lean

@@ -389,9 +389,9 @@ For `i ∈ [numParams, arity)`, we have that `result[i]` if this index of the in
 private def computeFixedIndexBitMask (numParams : Nat) (indType : InductiveType) (indFVars : Array Expr) : MetaM (Array Bool) := do
   let arity ← getArity indType
   if arity ≤ numParams then
-    return mkArray arity false
+    return .replicate arity false
   else
-    let maskRef ← IO.mkRef (mkArray numParams false ++ mkArray (arity - numParams) true)
+    let maskRef ← IO.mkRef (.replicate numParams false ++ .replicate (arity - numParams) true)
     let rec go (ctors : List Constructor) : MetaM (Array Bool) := do
       match ctors with
       | [] => maskRef.get

src/Lean/Elab/PreDefinition/FixedParams.lean

@@ -81,7 +81,7 @@ structure Info where
 
 def Info.init (revDeps : Array (Array (Array Nat))) : Info where
   graph := revDeps.map fun deps =>
-    mkArray deps.size (some (mkArray revDeps.size none))
+    .replicate deps.size (some (.replicate revDeps.size none))
   revDeps
 
 def Info.addSelfCalls (info : Info) : Info :=
@@ -309,7 +309,7 @@ scope.
 -/
 private partial def FixedParamPerm.forallTelescopeImpl (perm : FixedParamPerm)
     (type : Expr) (k : Array Expr → MetaM α) : MetaM α := do
-  go 0 type (mkArray perm.numFixed (mkSort 0))
+  go 0 type (.replicate perm.numFixed (mkSort 0))
 where
   go i type xs := do
     match perm[i]? with
@@ -382,7 +382,7 @@ def FixedParamPerm.pickFixed (perm : FixedParamPerm) (xs : Array α) : Array α
     pure #[]
   else
     let dummy := xs[0]
-    let ys := mkArray perm.numFixed dummy
+    let ys := .replicate perm.numFixed dummy
     go (perm.zip xs).toList ys
 where
   go | [], ys => return ys
@@ -437,7 +437,7 @@ def FixedParamPerms.fixedArePrefix (fixedParamPerms : FixedParamPerms) : Bool :=
   fixedParamPerms.perms.all fun paramInfos =>
     paramInfos ==
       (Array.range fixedParamPerms.numFixed).map Option.some ++
-      mkArray (paramInfos.size - fixedParamPerms.numFixed) .none
+      .replicate (paramInfos.size - fixedParamPerms.numFixed) .none
 
 /--
 If `xs` are the fixed parameters that are in scope, and `toErase` are, for each function, the
@@ -453,7 +453,7 @@ def FixedParamPerms.erase  (fixedParamPerms : FixedParamPerms) (xs : Array Expr)
   assert! fixedParamPerms.numFixed  = xs.size
   assert! toErase.size = fixedParamPerms.perms.size
   -- Calculate a mask on the fixed parameters of variables to erase
-  let mut mask := mkArray fixedParamPerms.numFixed false
+  let mut mask := Array.replicate fixedParamPerms.numFixed false
   for funIdx in [:toErase.size], paramIdxs in toErase, mapping in fixedParamPerms.perms do
     for paramIdx in paramIdxs do
       assert! paramIdx < mapping.size

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -77,7 +77,7 @@ private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat)
     let motiveTypes ← inferArgumentTypesN numTypeFormers pre
     let numMotives : Nat := positions.numIndices
     trace[Elab.definition.structural] "numMotives: {numMotives}"
-    let mut CTypes := Array.mkArray numMotives (.sort 37) -- dummy value
+    let mut CTypes := Array.replicate numMotives (.sort 37) -- dummy value
     for poss in positions, motiveType in motiveTypes do
       for pos in poss do
         CTypes := CTypes.set! pos motiveType
@@ -274,7 +274,7 @@ def inferBRecOnFTypes (recArgInfos : Array RecArgInfo) (positions : Positions)
     -- And return the types of the next arguments
     arrowDomainsN numTypeFormers brecOnType
 
-  let mut FTypes := Array.mkArray positions.numIndices (Expr.sort 0)
+  let mut FTypes := Array.replicate positions.numIndices (Expr.sort 0)
   for packedFType in packedFTypes, poss in positions do
     for pos in poss do
       FTypes := FTypes.set! pos packedFType

src/Lean/Elab/PreDefinition/Structural/Basic.lean

@@ -70,7 +70,7 @@ def Positions.numIndices (positions : Positions) : Nat :=
 `positions.inverse[k] = i` means that function `i` has type k
 -/
 def Positions.inverse (positions : Positions) : Array Nat := Id.run do
-  let mut r := mkArray positions.numIndices 0
+  let mut r := .replicate positions.numIndices 0
   for _h : i in [:positions.size] do
     for k in positions[i] do
       r := r.set! k i

src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean

@@ -47,7 +47,7 @@ arguments, and other parameters.
 -/
 def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array Expr × Array Expr) := Id.run do
   -- To simplify the index calculation, pad xs with dummy values where fixed parameters are
-  let xs := info.fixedParamPerm.buildArgs (mkArray info.fixedParamPerm.numFixed (mkSort 0)) xs
+  let xs := info.fixedParamPerm.buildArgs (.replicate info.fixedParamPerm.numFixed (mkSort 0)) xs
   -- First indices and major arg, using the order they appear in `info.indicesPos`
   let mut indexMajorArgs := #[]
   let indexMajorPos := info.indicesPos.push info.recArgPos

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -194,7 +194,7 @@ The close coupling with how arguments are packed and termination goals look like
 but it works for now.
 -/
 def groupGoalsByFunction (argsPacker : ArgsPacker) (numFuncs : Nat) (goals : Array MVarId) : MetaM (Array (Array MVarId)) := do
-  let mut r := mkArray numFuncs #[]
+  let mut r := .replicate numFuncs #[]
   for goal in goals do
     let type ← goal.getType
     let (.mdata _ (.app _ param)) := type

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -494,7 +494,7 @@ def RecCallCache.mk (funNames : Array Name) (decrTactics : Array (Option Decreas
   let decrTactic? := decrTactics[rcc.caller]!
   let callerMeasures := measuress[rcc.caller]!
   let calleeMeasures := measuress[rcc.callee]!
-  let cache ← IO.mkRef <| Array.mkArray callerMeasures.size (Array.mkArray calleeMeasures.size Option.none)
+  let cache ← IO.mkRef <| Array.replicate callerMeasures.size (Array.replicate calleeMeasures.size Option.none)
   return { callerName, decrTactic?, callerMeasures, calleeMeasures, rcc, cache }
 
 /-- Run `evalRecCall` and cache there result -/
@@ -551,7 +551,7 @@ where
   -- Enumerate all permissible uniform combinations
   goUniform (idx : Nat) : OptionT (StateM (Array (Array Nat))) Unit  := do
     if numMeasures.all (idx < ·) then
-      modify (·.push (Array.mkArray numMeasures.size idx))
+      modify (·.push (Array.replicate numMeasures.size idx))
       goUniform (idx + 1)
 
   -- Enumerate all other permissible combinations

src/Lean/Elab/Quotation.lean

@@ -411,7 +411,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
         let no ← no
         match k with
         | `optional =>
-          let nones := mkArray ids.size (← `(none))
+          let nones := .replicate ids.size (← `(none))
           `(let_delayed yes _ $ids* := $yes;
             if __discr.isNone then yes () $[ $nones]*
             else match __discr with

src/Lean/Elab/StructInst.lean

@@ -845,7 +845,9 @@ private partial def elabStructInstView (s : StructInstView) (expectedType? : Opt
             let val ← ensureHasType d val
             cont val { field with val := FieldVal.nested sNew } (instMVars ++ instMVarsNew)
         | .default  =>
-          match d.getAutoParamTactic? with
+          let some fieldInfo := getFieldInfo? env s.structName fieldName
+            | withRef field.ref <| throwFailedToElabField fieldName s.structName m!"no such field '{fieldName}'"
+          match fieldInfo.autoParam? with
           | some (.const tacticDecl ..) =>
             match evalSyntaxConstant env (← getOptions) tacticDecl with
             | .error err       => throwError err
@@ -855,7 +857,7 @@ private partial def elabStructInstView (s : StructInstView) (expectedType? : Opt
               -- We add info to get reliable positions for messages from evaluating the tactic script.
               let info := field.ref.getHeadInfo.nonCanonicalSynthetic
               let stx := stx.raw.rewriteBottomUp (·.setInfo info)
-              let type := (d.getArg! 0).consumeTypeAnnotations
+              let type := d.consumeTypeAnnotations
               let mvar ← mkTacticMVar type stx (.fieldAutoParam fieldName s.structName)
               -- Note(kmill): We are adding terminfo to simulate a previous implementation that elaborated `tacticBlock`.
               -- (See the aforementioned `processExplicitArg` for a comment about this.)
@@ -970,13 +972,23 @@ abbrev M := ReaderT Context (StateRefT State TermElabM)
 def isRoundDone : M Bool := do
   return (← get).progress && (← read).maxDistance > 0
 
-/-- Returns the `expr?` for the given field. -/
-def getFieldValue? (struct : StructInstView) (fieldName : Name) : Option Expr :=
-  struct.fields.findSome? fun field =>
-    if getFieldName field == fieldName then
-      field.expr?
-    else
-      none
+/-- Returns the `expr?` for the given field. The value may be inside a subobject. -/
+partial def getFieldValue? (struct : StructInstView) (fieldName : Name) : MetaM (Option Expr) := do
+  for field in struct.fields do
+    let fieldName' := getFieldName field
+    if fieldName' == fieldName then
+      return field.expr?
+    if let .nested s' := field.val then
+      if let some val ← getFieldValue? s' fieldName then
+        return val
+    if let some info := getFieldInfo? (← getEnv) struct.structName fieldName' then
+      if info.subobject?.isSome then
+        if let some e := field.expr? then
+          try
+            return ← mkProjection e fieldName
+          catch _ =>
+            pure ()
+  return none
 
 /-- Instantiates a default value from the given default value declaration, if applicable. -/
 partial def mkDefaultValue? (struct : StructInstView) (cinfo : ConstantInfo) : TermElabM (Option Expr) :=
@@ -988,7 +1000,7 @@ where
   | .lam n d b c => withRef struct.ref do
     if c.isExplicit then
       let fieldName := n
-      match getFieldValue? struct fieldName with
+      match ← getFieldValue? struct fieldName with
       | none     => return none
       | some val =>
         let valType ← inferType val
@@ -1078,8 +1090,9 @@ def tryToSynthesizeDefault (structs : Array StructInstView) (allStructNames : Ar
       return false
     else if h : i < structs.size then
       let struct := structs[i]
-      match getDefaultFnForField? (← getEnv) struct.structName fieldName with
+      match getEffectiveDefaultFnForField? (← getEnv) struct.structName fieldName with
       | some defFn =>
+        trace[Elab.struct] "default fn for '{fieldName}' is '{.ofConstName defFn}'"
         let cinfo ← getConstInfo defFn
         let mctx ← getMCtx
         match (← mkDefaultValue? struct cinfo) with
@@ -1141,7 +1154,7 @@ partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : StructInstV
         let env := (← getEnv)
         let structs := (← read).allStructNames
         missingFields.filter fun fieldName => structs.all fun struct =>
-          (getDefaultFnForField? env struct fieldName).isNone
+          (getEffectiveDefaultFnForField? env struct fieldName).isNone
       let fieldsToReport :=
         if missingFieldsWithoutDefault.isEmpty then missingFields else missingFieldsWithoutDefault
       throwErrorAt field.ref "fields missing: {fieldsToReport.toList.map (s!"'{·}'") |> ", ".intercalate}"

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean

@@ -50,10 +50,14 @@ where
   | .const val => mkApp2 (mkConst ``BVExpr.const) (toExpr w) (toExpr val)
   | .bin lhs op rhs => mkApp4 (mkConst ``BVExpr.bin) (toExpr w) (go lhs) (toExpr op) (go rhs)
   | .un op operand => mkApp3 (mkConst ``BVExpr.un) (toExpr w) (toExpr op) (go operand)
-  | .append (l := l) (r := r) lhs rhs =>
-    mkApp4 (mkConst ``BVExpr.append) (toExpr l) (toExpr r) (go lhs) (go rhs)
-  | .replicate (w := oldWidth) w inner =>
-    mkApp3 (mkConst ``BVExpr.replicate) (toExpr oldWidth) (toExpr w) (go inner)
+  | .append (w := w) (l := l) (r := r) lhs rhs _ =>
+    let wExpr := toExpr w
+    let proof := mkApp2 (mkConst ``Eq.refl [1]) (mkConst ``Nat) wExpr
+    mkApp6 (mkConst ``BVExpr.append) (toExpr l) (toExpr r) wExpr (go lhs) (go rhs) proof
+  | .replicate (w' := newWidth) (w := oldWidth) w inner _ =>
+    let newWExpr := toExpr newWidth
+    let proof := mkApp2 (mkConst ``Eq.refl [1]) (mkConst ``Nat) newWExpr
+    mkApp5 (mkConst ``BVExpr.replicate) (toExpr oldWidth) newWExpr (toExpr w) (go inner) proof
   | .extract (w := oldWidth) hi lo expr =>
     mkApp4 (mkConst ``BVExpr.extract) (toExpr oldWidth) (toExpr hi) (toExpr lo) (go expr)
   | .shiftLeft (m := m) (n := n) lhs rhs =>
@@ -296,6 +300,18 @@ structure LemmaState where
   The list of top level lemmas that got created on the fly during reflection.
   -/
   lemmas : Array SatAtBVLogical := #[]
+  /--
+  Cache for reification of `BVExpr`.
+  -/
+  bvExprCache : Std.HashMap Expr (Option ReifiedBVExpr) := {}
+  /--
+  Cache for reification of `BVPred`.
+  -/
+  bvPredCache : Std.HashMap Expr (Option ReifiedBVPred) := {}
+  /--
+  Cache for reification of `BVLogicalExpr`.
+  -/
+  bvLogicalCache : Std.HashMap Expr (Option ReifiedBVLogical) := {}
 
 /--
 The lemma reflection monad. It extends the usual reflection monad `M` by adding the ability to
@@ -315,6 +331,36 @@ Add another top level lemma.
 def addLemma (lemma : SatAtBVLogical) : LemmaM Unit := do
   modify fun s => { s with lemmas := s.lemmas.push lemma }
 
+@[specialize]
+def withBVExprCache (e : Expr) (f : Expr → LemmaM (Option ReifiedBVExpr)) :
+    LemmaM (Option ReifiedBVExpr) := do
+  match (← get).bvExprCache[e]? with
+  | some hit => return hit
+  | none =>
+    let res ← f e
+    modify fun s => { s with bvExprCache := s.bvExprCache.insert e res }
+    return res
+
+@[specialize]
+def withBVPredCache (e : Expr) (f : Expr → LemmaM (Option ReifiedBVPred)) :
+    LemmaM (Option ReifiedBVPred) := do
+  match (← get).bvPredCache[e]? with
+  | some hit => return hit
+  | none =>
+    let res ← f e
+    modify fun s => { s with bvPredCache := s.bvPredCache.insert e res }
+    return res
+
+@[specialize]
+def withBVLogicalCache (e : Expr) (f : Expr → LemmaM (Option ReifiedBVLogical)) :
+    LemmaM (Option ReifiedBVLogical) := do
+  match (← get).bvLogicalCache[e]? with
+  | some hit => return hit
+  | none =>
+    let res ← f e
+    modify fun s => { s with bvLogicalCache := s.bvLogicalCache.insert e res }
+    return res
+
 end LemmaM
 
 end Frontend

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean

@@ -85,11 +85,16 @@ where
     | HAppend.hAppend _ _ _ _ lhsExpr rhsExpr =>
       let some lhs ← goOrAtom lhsExpr | return none
       let some rhs ← goOrAtom rhsExpr | return none
-      let bvExpr := .append lhs.bvExpr rhs.bvExpr
-      let expr := mkApp4 (mkConst ``BVExpr.append)
-        (toExpr lhs.width)
-        (toExpr rhs.width)
-        lhs.expr rhs.expr
+      let bvExpr := .append lhs.bvExpr rhs.bvExpr rfl
+      let wExpr := toExpr (lhs.width + rhs.width)
+      let expr :=
+        mkApp6 (mkConst ``BVExpr.append)
+          (toExpr lhs.width)
+          (toExpr rhs.width)
+          wExpr
+          lhs.expr
+          rhs.expr
+          (← mkEqRefl wExpr)
       let proof := do
         let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr
         let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr
@@ -108,11 +113,15 @@ where
     | BitVec.replicate _ nExpr innerExpr =>
       let some inner ← goOrAtom innerExpr | return none
       let some n ← getNatValue? nExpr | return none
-      let bvExpr := .replicate n inner.bvExpr
-      let expr := mkApp3 (mkConst ``BVExpr.replicate)
-        (toExpr inner.width)
-        (toExpr n)
-        inner.expr
+      let bvExpr := .replicate n inner.bvExpr rfl
+      let newWExpr := toExpr (inner.width * n)
+      let expr :=
+        mkApp5 (mkConst ``BVExpr.replicate)
+          (toExpr inner.width)
+          newWExpr
+          (toExpr n)
+          inner.expr
+          (← mkEqRefl newWExpr)
       let proof := do
         let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
         -- This is safe as `replicate_congr` holds definitionally if the arguments are defeq.
@@ -175,10 +184,11 @@ where
   to return `some`.
   -/
   goOrAtom (x : Expr) : LemmaM (Option ReifiedBVExpr) := do
-    let res ← go x
-    match res with
-    | some exp => return some exp
-    | none => ReifiedBVExpr.bitVecAtom x false
+    LemmaM.withBVExprCache x fun x => do
+      let res ← go x
+      match res with
+      | some exp => return some exp
+      | none => ReifiedBVExpr.bitVecAtom x false
 
   shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
       (shiftOpName : Name) (congrThm : Name) :
@@ -274,9 +284,10 @@ Reify an `Expr` that is a predicate about `BitVec`.
 Unless this function is called on something that is not a `Bool` it is always going to return `some`.
 -/
 partial def ReifiedBVPred.of (t : Expr) : LemmaM (Option ReifiedBVPred) := do
-  match ← go t with
-  | some pred => return some pred
-  | none => ReifiedBVPred.boolAtom t
+  LemmaM.withBVPredCache t fun t => do
+    match ← go t with
+    | some pred => return some pred
+    | none => ReifiedBVPred.boolAtom t
 where
   /--
   Reify `t`, returns `none` if the reification procedure failed.
@@ -335,9 +346,10 @@ where
   Unless this function is called on something that is not a `Bool` it is always going to return `some`.
   -/
   goOrAtom (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
-    match ← go t with
-    | some boolExpr => return some boolExpr
-    | none => ReifiedBVLogical.boolAtom t
+    LemmaM.withBVLogicalCache t fun t => do
+      match ← go t with
+      | some boolExpr => return some boolExpr
+      | none => ReifiedBVLogical.boolAtom t
 
   gateReflection (lhsExpr rhsExpr : Expr) (gate : Gate) :
       LemmaM (Option ReifiedBVLogical) := do

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean

@@ -16,6 +16,7 @@ import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Structures
 import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.IntToBitVec
 import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Enums
 import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.TypeAnalysis
+import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.ShortCircuit
 
 /-!
 This module contains the implementation of `bv_normalize`, the preprocessing tactic for `bv_decide`.
@@ -87,7 +88,15 @@ where
 
     trace[Meta.Tactic.bv] m!"Running fixpoint pipeline on:\n{g}"
     let pipeline ← passPipeline
-    Pass.fixpointPipeline pipeline g
+    let some g' ← Pass.fixpointPipeline pipeline g | return none
+    /-
+    Run short circuiting once post fixpoint, as it increases the size of terms with
+    the aim of exposing potential short-circuit reasoning to the solver.
+    -/
+    if cfg.shortCircuit then
+      shortCircuitPass |>.run g'
+    else
+      return g'
 
 @[builtin_tactic Lean.Parser.Tactic.bvNormalize]
 def evalBVNormalize : Tactic := fun

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean

@@ -439,6 +439,10 @@ partial def enumsPass : Pass where
       if cfg.structures then
         (simprocs, relevantLemmas) ← addStructureSimpLemmas simprocs relevantLemmas
 
+      -- same for fixed integers
+      if cfg.fixedInt then
+        relevantLemmas := relevantLemmas.push (← intToBitVecExt.getTheorems)
+
       let simpCtx ← Simp.mkContext
         (config := {
           failIfUnchanged := false,

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/ShortCircuit.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2025 Tobias Grosser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tobias Grosser
+-/
+prelude
+import Lean.Elab.Tactic.Simp
+import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Basic
+import Lean.Elab.Tactic.BVDecide.Frontend.Attr
+import Std.Tactic.BVDecide.Normalize.BitVec
+
+/-!
+This module contains the implementation of the short-circuiting pass, which is responsible for
+applying short-circuit optimizations for `*`, e.g., translating `x1 * y == x2 * y` to
+`!(!x1 == x2 && !x1 * y == x2 * y)`.
+-/
+
+namespace Lean.Elab.Tactic.BVDecide
+namespace Frontend.Normalize
+
+open Lean.Meta
+open Std.Tactic.BVDecide.Normalize.BitVec
+
+/--
+Responsible for applying short-circuit optimizations for `*`, e.g.,
+translating `x1 * y == x2 * y` to `!(!x1 == x2 && !x1 * y == x2 * y)`.
+-/
+def shortCircuitPass : Pass where
+  name := `shortCircuitPass
+  run' goal := do
+    goal.withContext do
+      let mut theorems : SimpTheoremsArray := #[]
+      theorems ← theorems.addTheorem
+        (Lean.Meta.Origin.decl `mul_beq_mul_short_circuit_left)
+        (mkConst ``mul_beq_mul_short_circuit_left)
+      theorems ← theorems.addTheorem
+        (Lean.Meta.Origin.decl `mul_beq_mul_short_circuit_right)
+        (mkConst ``mul_beq_mul_short_circuit_right)
+
+      let simpCtx ← Simp.mkContext
+        (config := {
+          failIfUnchanged := false,
+          zetaDelta := true,
+          singlePass := true,
+          maxSteps := (← PreProcessM.getConfig).maxSteps
+        })
+        (simpTheorems := theorems)
+        (congrTheorems := (← getSimpCongrTheorems))
+
+      let hyps ← getPropHyps
+      let ⟨result?, _⟩ ← simpGoal goal
+        (ctx := simpCtx)
+        (simprocs := #[])
+        (fvarIdsToSimp := hyps)
+      let some (_, newGoal) := result? | return none
+      return newGoal
+
+end Frontend.Normalize
+end Lean.Elab.Tactic.BVDecide

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean

@@ -457,5 +457,27 @@ builtin_simproc [bv_normalize] bv_extract_concat
     -- extract is not limited to side
     return .continue
 
+builtin_simproc [bv_normalize] extract_add
+    (BitVec.extractLsb' _ _ ((_ : BitVec _) + (_ : BitVec _))) := fun e => do
+  let_expr BitVec.extractLsb' widthExpr startExpr lenExpr targetExpr := e | return .continue
+  let_expr HAdd.hAdd _ _ _ _ lhsExpr rhsExpr := targetExpr | return .continue
+  let some start ← getNatValue? startExpr | return .continue
+  let some len ← getNatValue? lenExpr | return .continue
+  let some width ← getNatValue? widthExpr | return .continue
+  if !(start == 0 && len ≤ width) then return .continue
+
+  let newLhsExpr := mkApp4 (mkConst ``BitVec.extractLsb') widthExpr startExpr lenExpr lhsExpr
+  let newRhsExpr := mkApp4 (mkConst ``BitVec.extractLsb') widthExpr startExpr lenExpr rhsExpr
+  let expr ← mkAdd newLhsExpr newRhsExpr
+  let proof :=
+    mkApp5
+      (mkConst ``BitVec.extractLsb'_add)
+      widthExpr
+      lenExpr
+      lhsExpr
+      rhsExpr
+      (← mkDecideProof (← mkLe lenExpr widthExpr))
+  return .visit { expr := expr, proof? := some proof }
+
 end Frontend.Normalize
 end Lean.Elab.Tactic.BVDecide

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

@@ -80,7 +80,7 @@ def run (proof : Array IntAction) (x : M α) : Except String α := do
     | .del .. => acc
   let proof := proof.foldl (init := {}) folder
   let used := Nat.fold proof.size (init := ByteArray.emptyWithCapacity proof.size) (fun _ _ acc => acc.push 0)
-  let mapped := Array.mkArray proof.size 0
+  let mapped := Array.replicate proof.size 0
   return ReaderT.run x { proof, initialId, addEmptyId } |>.run' { used, mapped }
 
 @[inline]

src/Lean/Elab/Tactic/Basic.lean

@@ -35,7 +35,19 @@ structure Context where
   -/
   recover    : Bool := true
 
+/--
+The tactic monad, which extends the term elaboration monad `TermElabM` with state that contains the
+current goals (`Lean.Elab.Tactic.State`, accessible via `MonadStateOf`) and local information about
+the current tactic's name and whether error recovery is enabled (`Lean.Elab.Tactic.Context`,
+accessible via `MonadReaderOf`).
+-/
 abbrev TacticM := ReaderT Context $ StateRefT State TermElabM
+/--
+A tactic is a function from syntax to an action in the tactic monad.
+
+A given tactic syntax kind may have multiple `Tactic`s associated with it, all of which will be
+attempted until one succeeds.
+-/
 abbrev Tactic  := Syntax → TacticM Unit
 
 /-

src/Lean/Elab/Tactic/Ext.lean

@@ -110,7 +110,7 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl
         let type ← mkExtType structName flat
         let pf ← withSynthesize do
           let indVal ← getConstInfoInduct structName
-          let params := Array.mkArray indVal.numParams (← `(_))
+          let params := Array.replicate indVal.numParams (← `(_))
           Elab.Term.elabTermEnsuringType (expectedType? := type) (implicitLambda := false)
             -- introduce the params, do cases on 'x' and 'y', and then substitute each equation
             (← `(by intro $params* {..} {..}; intros; subst_eqs; rfl))

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -595,7 +595,7 @@ where
       |> String.join
 
   mentioned (atoms : Array Expr) (constraints : Std.HashMap Coeffs Fact) : MetaM (Array Bool) := do
-    let initMask := Array.mkArray atoms.size false
+    let initMask := .replicate atoms.size false
     return constraints.fold (init := initMask) fun mask coeffs _ =>
       coeffs.zipIdx.foldl (init := mask) fun mask (c, i) =>
         if c = 0 then mask else mask.set! i true

src/Lean/Environment.lean

@@ -9,7 +9,6 @@ import Init.Data.Array.BinSearch
 import Init.Data.Stream
 import Init.System.Promise
 import Lean.ImportingFlag
-import Lean.Data.HashMap
 import Lean.Data.NameTrie
 import Lean.Data.SMap
 import Lean.Declaration
@@ -1636,7 +1635,7 @@ private def setImportedEntries (env : Environment) (mods : Array ModuleData) (st
   for extDescr in extDescrs[startingAt:] do
     -- safety: as in `modifyState`
     states := unsafe extDescr.toEnvExtension.modifyStateImpl states fun s =>
-      { s with importedEntries := mkArray mods.size #[] }
+      { s with importedEntries := .replicate mods.size #[] }
   /- For each module `mod`, and `mod.entries`, if the extension name is one of the extensions after `startingAt`, set `entries` -/
   let extNameIdx ← mkExtNameMap startingAt
   for h : modIdx in [:mods.size] do

src/Lean/Expr.lean

@@ -1136,7 +1136,7 @@ private def getAppArgsAux : Expr → Array Expr → Nat → Array Expr
 @[inline] def getAppArgs (e : Expr) : Array Expr :=
   let dummy := mkSort levelZero
   let nargs := e.getAppNumArgs
-  getAppArgsAux e (mkArray nargs dummy) (nargs-1)
+  getAppArgsAux e (.replicate nargs dummy) (nargs-1)
 
 private def getBoundedAppArgsAux : Expr → Array Expr → Nat → Array Expr
   | app f a, as, i + 1 => getBoundedAppArgsAux f (as.set! i a) i
@@ -1151,7 +1151,7 @@ where `k` is minimal such that the size of this array is at most `maxArgs`.
 @[inline] def getBoundedAppArgs (maxArgs : Nat) (e : Expr) : Array Expr :=
   let dummy := mkSort levelZero
   let nargs := min maxArgs e.getAppNumArgs
-  getBoundedAppArgsAux e (mkArray nargs dummy) nargs
+  getBoundedAppArgsAux e (.replicate nargs dummy) nargs
 
 private def getAppRevArgsAux : Expr → Array Expr → Array Expr
   | app f a, as => getAppRevArgsAux f (as.push a)
@@ -1169,7 +1169,7 @@ private def getAppRevArgsAux : Expr → Array Expr → Array Expr
 @[inline] def withApp (e : Expr) (k : Expr → Array Expr → α) : α :=
   let dummy := mkSort levelZero
   let nargs := e.getAppNumArgs
-  withAppAux k e (mkArray nargs dummy) (nargs-1)
+  withAppAux k e (.replicate nargs dummy) (nargs-1)
 
 /-- Return the function (name) and arguments of an application. -/
 def getAppFnArgs (e : Expr) : Name × Array Expr :=
@@ -1182,7 +1182,7 @@ The resulting array has size `n` even if `f.getAppNumArgs < n`.
 -/
 @[inline] def getAppArgsN (e : Expr) (n : Nat) : Array Expr :=
   let dummy := mkSort levelZero
-  loop n e (mkArray n dummy)
+  loop n e (.replicate n dummy)
 where
   loop : Nat → Expr → Array Expr → Array Expr
     | 0,   _,        as => as

src/Lean/Language/Lean.lean

@@ -645,7 +645,7 @@ where
         let infoTree := infoSt.trees[0]!
         let opts := cmdState.scopes.head!.opts
         let mut msgLog := MessageLog.empty
-        if (← isTracingEnabledForCore `Elab.info opts) then
+        if checkTraceOption (← inheritedTraceOptions.get) opts `Elab.info then
           if let .ok msg ← infoTree.format.toBaseIO then
             let data := .tagged `trace <| .trace { cls := `Elab.info } .nil #[msg]
             msgLog := msgLog.add {
@@ -661,7 +661,7 @@ where
 
       -- report traces when *all* tasks are finished
       let traceTask ←
-        if (← isTracingEnabledForCore `Elab.snapshotTree cmdState.scopes.head!.opts) then
+        if checkTraceOption (← inheritedTraceOptions.get) cmdState.scopes.head!.opts `Elab.snapshotTree then
           -- We want to trace all of `CommandParsedSnapshot` but `traceTask` is part of it, so let's
           -- create a temporary snapshot tree containing all tasks but it
           let snaps := #[

src/Lean/Level.lean

@@ -5,8 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.QSort
-import Lean.Data.HashMap
-import Lean.Data.HashSet
 import Lean.Data.PersistentHashMap
 import Lean.Data.PersistentHashSet
 import Lean.Hygiene

src/Lean/Linter/List.lean

@@ -106,8 +106,8 @@ def numericalWidths (t : InfoTree) : List (Syntax × Name) :=
     if let .ofTermInfo info := info then
       let idxs := match_expr info.expr with
       | List.replicate _ n _ => [n]
-      | Array.mkArray _ n _ => [n]
-      | Vector.mkVector _ n _ => [n]
+      | Array.replicate _ n _ => [n]
+      | Vector.replicate _ n _ => [n]
       | List.range n => [n]
       | List.range' _ n _ => [n]
       | Array.range n => [n]

src/Lean/Meta/Canonicalizer.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Data.HashMap
 import Lean.Util.ShareCommon
 import Lean.Meta.Basic
 import Lean.Meta.FunInfo

src/Lean/Meta/IndPredBelow.lean

@@ -441,7 +441,7 @@ partial def mkBelowMatcher
   withExistingLocalDecls (lhss.foldl (init := []) fun s v => s ++ v.fvarDecls) do
     for lhs in lhss do
       trace[Meta.IndPredBelow.match] "{lhs.patterns.map (·.toMessageData)}"
-  let res ← Match.mkMatcher (exceptionIfContainsSorry := true) { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
+  let res ← Match.mkMatcher (exceptionIfContainsSorry := true) { matcherName, matchType, discrInfos := .replicate (mkMatcherInput.numDiscrs + 1) {}, lhss }
   res.addMatcher
   -- if a wrong index is picked, the resulting matcher can be type-incorrect.
   -- we check here, so that errors can propagate higher up the call stack.
@@ -491,7 +491,7 @@ where
       -- `belowCtor` carries a `below`, a non-`below` and a `motive` version of each
       -- field that occurs in a recursive application of the inductive predicate.
       -- `belowIndices` is a mapping from non-`below` to the `below` version of each field.
-      let mut belowFieldOpts := mkArray belowCtor.numFields none
+      let mut belowFieldOpts := .replicate belowCtor.numFields none
       let fields := fields.toArray
       for fieldIdx in [:fields.size] do
         belowFieldOpts := belowFieldOpts.set! belowIndices[fieldIdx]! (some fields[fieldIdx]!)

src/Lean/Meta/Match/MatcherApp/Basic.lean

@@ -54,7 +54,7 @@ def matchMatcherApp? [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (alsoCases
       let params     := args[:info.numParams]
       let motive     := args[info.numParams]!
       let discrs     := args[info.numParams + 1 : info.numParams + 1 + info.numIndices + 1]
-      let discrInfos := Array.mkArray (info.numIndices + 1) {}
+      let discrInfos := .replicate (info.numIndices + 1) {}
       let alts       := args[info.numParams + 1 + info.numIndices + 1 : info.numParams + 1 + info.numIndices + 1 + info.numCtors]
       let remaining  := args[info.numParams + 1 + info.numIndices + 1 + info.numCtors :]
       let uElimPos?  := if info.levelParams.length == declLevels.length then none else some 0

src/Lean/Meta/SizeOf.lean

@@ -196,7 +196,7 @@ def mkSizeOfSpecLemmaInstance (ctorApp : Expr) : MetaM Expr :=
     let lemmaInfo  ← getConstInfo lemmaName
     let lemmaArity ← forallTelescopeReducing lemmaInfo.type fun xs _ => return xs.size
     let lemmaArgMask := ctorParams.toArray.map some
-    let lemmaArgMask := lemmaArgMask ++ mkArray (lemmaArity - ctorInfo.numParams - ctorInfo.numFields) (none (α := Expr))
+    let lemmaArgMask := lemmaArgMask ++ .replicate (lemmaArity - ctorInfo.numParams - ctorInfo.numFields) (none (α := Expr))
     let lemmaArgMask := lemmaArgMask ++ ctorFields.toArray.map some
     mkAppOptM lemmaName lemmaArgMask
 

src/Lean/Meta/Tactic/FunInd.lean

@@ -1133,11 +1133,18 @@ where doRealize inductName := do
     { name := inductName, levelParams := us, type := eTyp, value := e' }
 
   if names.size = 1 then
+    let mut params := #[]
+    for h : i in [:fixedParamPerms.perms[0]!.size] do
+      if let some idx := fixedParamPerms.perms[0]![i] then
+        if paramMask[idx]! then
+          params := params.push .param
+        else
+          params := params.push .dropped
+      else
+        params := params.push .target
+
     setFunIndInfo {
-      funIndName := inductName
-      levelMask := usMask
-      params := paramMask.map (cond · .param .dropped) ++
-        mkArray motiveArities[0]! .target
+      funIndName := inductName, levelMask := usMask, params := params
     }
 
 
@@ -1206,7 +1213,7 @@ def deriveCases (name : Name) : MetaM Unit := do
     setFunIndInfo {
       funIndName := casesName
       levelMask := usMask
-      params := mkArray motiveArity .target
+      params := .replicate motiveArity .target
     }
 
 

src/Lean/Meta/Tactic/Grind.lean

@@ -29,6 +29,7 @@ import Lean.Meta.Tactic.Grind.Ext
 import Lean.Meta.Tactic.Grind.MatchCond
 import Lean.Meta.Tactic.Grind.MatchDiscrOnly
 import Lean.Meta.Tactic.Grind.Diseq
+import Lean.Meta.Tactic.Grind.MBTC
 
 namespace Lean
 
@@ -50,6 +51,7 @@ builtin_initialize registerTraceClass `grind.split
 builtin_initialize registerTraceClass `grind.split.candidate
 builtin_initialize registerTraceClass `grind.split.resolved
 builtin_initialize registerTraceClass `grind.beta
+builtin_initialize registerTraceClass `grind.mbtc
 
 /-! Trace options for `grind` developers -/
 builtin_initialize registerTraceClass `grind.debug
@@ -68,5 +70,6 @@ builtin_initialize registerTraceClass `grind.debug.internalize
 builtin_initialize registerTraceClass `grind.debug.matchCond
 builtin_initialize registerTraceClass `grind.debug.matchCond.lambda
 builtin_initialize registerTraceClass `grind.debug.matchCond.proveFalse
+builtin_initialize registerTraceClass `grind.debug.mbtc
 
 end Lean

src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean

@@ -16,6 +16,7 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.SearchM
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.MBTC
 
 namespace Lean
 

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Combinators
+import Lean.Meta.Tactic.Grind.Canon
+import Lean.Meta.Tactic.Grind.MBTC
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
+
+namespace Lean.Meta.Grind.Arith.Cutsat
+
+private def getAssignmentExt? (e : Expr) : GoalM (Option Rat) := do
+  let val? ← getAssignment? (← get) (← getENode e)
+  if val?.isSome then
+    return val?
+  let type ← inferType e
+  if type == Nat.mkType then
+    for parent in (← getParents e) do
+      let_expr NatCast.natCast _ inst _ := parent | pure ()
+      let_expr instNatCastInt := inst | pure ()
+      return (← getAssignment? (← get) (← getENode parent))
+  return none
+
+private def hasTheoryVar (e : Expr) : GoalM Bool := do
+  return (← getAssignmentExt? e).isSome
+
+private def isInterpreted (e : Expr) : GoalM Bool := do
+  if isInterpretedTerm e then return true
+  let f := e.getAppFn
+  return f.isConstOf ``LE.le || f.isConstOf ``Dvd.dvd
+
+private def eqAssignment (a b : Expr) : GoalM Bool := do
+  let some v₁ ← getAssignmentExt? a | return false
+  let some v₂ ← getAssignmentExt? b | return false
+  return v₁ == v₂
+
+def mbtcTac : GrindTactic :=
+  Grind.mbtcTac {
+    hasTheoryVar := hasTheoryVar
+    isInterpreted := isInterpreted
+    eqAssignment := eqAssignment
+  }
+
+end Lean.Meta.Grind.Arith.Cutsat

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean

@@ -53,7 +53,7 @@ where
     else
       go (next + 1)
 
-private def isInterpretedTerm (e : Expr) : Bool :=
+def isInterpretedTerm (e : Expr) : Bool :=
   isNatNum e || isIntNum e || e.isAppOf ``HAdd.hAdd || e.isAppOf ``HMul.hMul || e.isAppOf ``HSub.hSub
   || e.isAppOf ``Neg.neg || e.isAppOf ``HDiv.hDiv || e.isAppOf ``HMod.hMod
   || e.isAppOf ``NatCast.natCast || e.isIte || e.isDIte
@@ -69,7 +69,7 @@ private def assignEqc (goal : Goal) (e : Expr) (v : Rat) (a : Std.HashMap Expr R
     a := a.insert e v
   return a
 
-private def getAssignment? (goal : Goal) (node : ENode) : MetaM (Option Rat) := do
+def getAssignment? (goal : Goal) (node : ENode) : MetaM (Option Rat) := do
   assert! isSameExpr node.self node.root
   if let some v := getCutsatAssignment? goal node then
     return some v

src/Lean/Meta/Tactic/Grind/Arith/Offset/Model.lean

@@ -16,12 +16,12 @@ def mkModel (goal : Goal) : MetaM (Array (Expr × Nat)) := do
   let dbg := grind.debug.get (← getOptions)
   let nodes := s.nodes
   let isInterpreted (u : Nat) : Bool := isNatNum s.nodes[u]!
-  let mut pre : Array (Option Int) := mkArray nodes.size none
+  let mut pre : Array (Option Int) := .replicate nodes.size none
   /-
   `needAdjust[u]` is true if `u` assignment is not connected to an interpreted value in the graph.
   That is, its assignment may be negative.
   -/
-  let mut needAdjust : Array Bool := mkArray nodes.size true
+  let mut needAdjust : Array Bool := .replicate nodes.size true
   -- Initialize `needAdjust`
   for u in [: nodes.size] do
     if isInterpreted u then

src/Lean/Meta/Tactic/Grind/Arith/Offset/Types.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Data.AssocList
 import Lean.Data.PersistentArray
 import Lean.Meta.Tactic.Grind.ENodeKey
 import Lean.Meta.Tactic.Grind.Arith.Util