chore: upstream Array.reduceOption

.github/workflows/check-prelude.yml

@@ -11,9 +11,7 @@ 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 }}
-          sparse-checkout: |
-            src/Lean
-            src/Std
+          sparse-checkout: src/Lean
       - name: Check Prelude
         run: |
           failed_files=""
@@ -21,8 +19,8 @@ jobs:
             if ! grep -q "^prelude$" "$file"; then
               failed_files="$failed_files$file\n"
             fi
-          done < <(find src/Lean src/Std -name '*.lean' -print0)
+          done < <(find src/Lean -name '*.lean' -print0)
           if [ -n "$failed_files" ]; then
             echo -e "The following files should use 'prelude':\n$failed_files"
             exit 1
-          fi
+          fi

CODEOWNERS

@@ -4,14 +4,14 @@
 # Listed persons will automatically be asked by GitHub to review a PR touching these paths.
 # If multiple names are listed, a review by any of them is considered sufficient by default.
 
-/.github/ @Kha @kim-em
-/RELEASES.md @kim-em
+/.github/ @Kha @semorrison
+/RELEASES.md @semorrison
 /src/kernel/ @leodemoura
 /src/lake/ @tydeu
 /src/Lean/Compiler/ @leodemoura
 /src/Lean/Data/Lsp/ @mhuisi
-/src/Lean/Elab/Deriving/ @kim-em
-/src/Lean/Elab/Tactic/ @kim-em
+/src/Lean/Elab/Deriving/ @semorrison
+/src/Lean/Elab/Tactic/ @semorrison
 /src/Lean/Language/ @Kha
 /src/Lean/Meta/Tactic/ @leodemoura
 /src/Lean/Parser/ @Kha
@@ -19,7 +19,7 @@
 /src/Lean/PrettyPrinter/Delaborator/ @kmill
 /src/Lean/Server/ @mhuisi
 /src/Lean/Widget/ @Vtec234
-/src/Init/Data/ @kim-em
+/src/Init/Data/ @semorrison
 /src/Init/Data/Array/Lemmas.lean @digama0
 /src/Init/Data/List/Lemmas.lean @digama0
 /src/Init/Data/List/BasicAux.lean @digama0
@@ -45,4 +45,3 @@
 /src/Std/ @TwoFX
 /src/Std/Tactic/BVDecide/ @hargoniX
 /src/Lean/Elab/Tactic/BVDecide/ @hargoniX
-/src/Std/Sat/ @hargoniX

src/Init.lean

@@ -35,4 +35,3 @@ import Init.Ext
 import Init.Omega
 import Init.MacroTrace
 import Init.Grind
-import Init.While

src/Init/Data/Array/Basic.lean

@@ -25,8 +25,6 @@ variable {α : Type u}
 
 namespace Array
 
-@[deprecated size (since := "2024-10-13")] abbrev data := @toList
-
 /-! ### Preliminary theorems -/
 
 @[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
@@ -80,26 +78,6 @@ theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
 
 @[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
 
-@[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
-
-end Array
-
-namespace List
-
-@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
-
-@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
-    a.toArray[i] = a[i]'(by simpa using h) := rfl
-
-@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
-
-@[simp] theorem getElem!_toArray [Inhabited α] {a : List α} {i : Nat} :
-    a.toArray[i]! = a[i]! := rfl
-
-end List
-
-namespace Array
-
 @[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
 
 @[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
@@ -418,25 +396,20 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
-/-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/
 @[inline]
-def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
-    (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=
+def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=
   let rec @[specialize] map (i : Nat) (j : Nat) (inv : i + j = as.size) (bs : Array β) : m (Array β) := do
     match i, inv with
     | 0,    _  => pure bs
     | i+1, inv =>
-      have j_lt : j < as.size := by
+      have : j < as.size := by
         rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm]
         apply Nat.le_add_right
+      let idx : Fin as.size := ⟨j, this⟩
       have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
-      map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get ⟨j, j_lt⟩)))
+      map i (j+1) this (bs.push (← f idx (as.get idx)))
   map as.size 0 rfl (mkEmpty as.size)
 
-@[inline]
-def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Nat → α → m β) : m (Array β) :=
-  as.mapFinIdxM fun i a => f i a
-
 @[inline]
 def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β) := do
   for a in as do
@@ -542,13 +515,8 @@ def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : A
 def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β :=
   Id.run <| as.mapM f
 
-/-- Variant of `mapIdx` which receives the index as a `Fin as.size`. -/
 @[inline]
-def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
-  Id.run <| as.mapFinIdxM f
-
-@[inline]
-def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Nat → α → β) : Array β :=
+def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
   Id.run <| as.mapIdxM f
 
 /-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/

src/Init/Data/Array/Bootstrap.lean

@@ -42,7 +42,7 @@ theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
   unfold foldrM.fold
   match i with
   | 0 => simp [List.foldlM, List.take]
-  | i+1 => rw [← List.take_concat_get _ _ h]; simp [← (aux f arr · i)]
+  | i+1 => rw [← List.take_concat_get _ _ h]; simp [← (aux f arr · i)]; rfl
 
 theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init : β) (arr : Array α) :
     arr.foldrM f init = arr.toList.reverse.foldlM (fun x y => f y x) init := by

src/Init/Data/Array/DecidableEq.lean

@@ -6,8 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.Basic
 import Init.Data.BEq
-import Init.Data.Nat.Lemmas
-import Init.Data.List.Nat.BEq
 import Init.ByCases
 
 namespace Array
@@ -28,14 +26,6 @@ theorem rel_of_isEqvAux
       subst hj'
       exact heqv.left
 
-theorem isEqvAux_of_rel (r : α → α → Bool) (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size)
-    (w : ∀ j, (hj : j < i) → r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi)))) : Array.isEqvAux a b hsz r i hi := by
-  induction i with
-  | zero => simp [Array.isEqvAux]
-  | succ i ih =>
-    simp only [isEqvAux, Bool.and_eq_true]
-    exact ⟨w i (Nat.lt_add_one i), ih _ fun j hj => w j (Nat.lt_add_right 1 hj)⟩
-
 theorem rel_of_isEqv (r : α → α → Bool) (a b : Array α) :
     Array.isEqv a b r → ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) := by
   simp only [isEqv]
@@ -43,29 +33,6 @@ theorem rel_of_isEqv (r : α → α → Bool) (a b : Array α) :
   · exact fun h' => ⟨h, rel_of_isEqvAux r a b h a.size (Nat.le_refl ..) h'⟩
   · intro; contradiction
 
-theorem isEqv_iff_rel (a b : Array α) (r) :
-    Array.isEqv a b r ↔ ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) :=
-  ⟨rel_of_isEqv r a b, fun ⟨h, w⟩ => by
-    simp only [isEqv, ← h, ↓reduceDIte]
-    exact isEqvAux_of_rel r a b h a.size (by simp [h]) w⟩
-
-theorem isEqv_eq_decide (a b : Array α) (r) :
-    Array.isEqv a b r =
-      if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h'))) else false := by
-  by_cases h : Array.isEqv a b r
-  · simp only [h, Bool.true_eq]
-    simp only [isEqv_iff_rel] at h
-    obtain ⟨h, w⟩ := h
-    simp [h, w]
-  · let h' := h
-    simp only [Bool.not_eq_true] at h
-    simp only [h, Bool.false_eq, dite_eq_right_iff, decide_eq_false_iff_not, Classical.not_forall,
-      Bool.not_eq_true]
-    simpa [isEqv_iff_rel] using h'
-
-@[simp] theorem isEqv_toList [BEq α] (a b : Array α) : (a.toList.isEqv b.toList r) = (a.isEqv b r) := by
-  simp [isEqv_eq_decide, List.isEqv_eq_decide]
-
 theorem eq_of_isEqv [DecidableEq α] (a b : Array α) (h : Array.isEqv a b (fun x y => x = y)) : a = b := by
   have ⟨h, h'⟩ := rel_of_isEqv (fun x y => x = y) a b h
   exact ext _ _ h (fun i lt _ => by simpa using h' i lt)
@@ -89,22 +56,4 @@ instance [DecidableEq α] : DecidableEq (Array α) :=
     | true  => isTrue (eq_of_isEqv a b h)
     | false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction
 
-theorem beq_eq_decide [BEq α] (a b : Array α) :
-    (a == b) = if h : a.size = b.size then
-      decide (∀ (i : Nat) (h' : i < a.size), a[i] == b[i]'(h ▸ h')) else false := by
-  simp [BEq.beq, isEqv_eq_decide]
-
-@[simp] theorem beq_toList [BEq α] (a b : Array α) : (a.toList == b.toList) = (a == b) := by
-  simp [beq_eq_decide, List.beq_eq_decide]
-
 end Array
-
-namespace List
-
-@[simp] theorem isEqv_toArray [BEq α] (a b : List α) : (a.toArray.isEqv b.toArray r) = (a.isEqv b r) := by
-  simp [isEqv_eq_decide, Array.isEqv_eq_decide]
-
-@[simp] theorem beq_toArray [BEq α] (a b : List α) : (a.toArray == b.toArray) = (a == b) := by
-  simp [beq_eq_decide, Array.beq_eq_decide]
-
-end List

src/Init/Data/Array/GetLit.lean

@@ -41,6 +41,6 @@ where
   getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
     rfl
   go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
-    induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.get_drop_eq_drop, *]
+    induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
 
 end Array

src/Init/Data/Array/Lemmas.lean

@@ -8,8 +8,6 @@ import Init.Data.Nat.Lemmas
 import Init.Data.List.Impl
 import Init.Data.List.Monadic
 import Init.Data.List.Range
-import Init.Data.List.Nat.TakeDrop
-import Init.Data.List.Nat.Modify
 import Init.Data.Array.Mem
 import Init.TacticsExtra
 
@@ -19,6 +17,8 @@ import Init.TacticsExtra
 
 namespace Array
 
+@[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
+
 @[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl
 
 theorem getElem_eq_getElem_toList {a : Array α} (h : i < a.size) : a[i] = a.toList[i] := by
@@ -43,32 +43,21 @@ theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[
   rw [getElem?_eq]
   split <;> simp_all
 
-theorem getElem_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
+theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
     (a.push x)[i] = a[i] := by
   simp only [push, getElem_eq_getElem_toList, List.concat_eq_append, List.getElem_append_left, h]
 
-@[simp] theorem getElem_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
+@[simp] theorem get_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
   simp only [push, getElem_eq_getElem_toList, List.concat_eq_append]
   rw [List.getElem_append_right] <;> simp [getElem_eq_getElem_toList, Nat.zero_lt_one]
 
-theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
+theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
     (a.push x)[i] = if h : i < a.size then a[i] else x := by
   by_cases h' : i < a.size
-  · simp [getElem_push_lt, h']
+  · simp [get_push_lt, h']
   · simp at h
-    simp [getElem_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
-
-@[deprecated getElem_push (since := "2024-10-21")] abbrev get_push := @getElem_push
-@[deprecated getElem_push_lt (since := "2024-10-21")] abbrev get_push_lt := @getElem_push_lt
-@[deprecated getElem_push_eq (since := "2024-10-21")] abbrev get_push_eq := @getElem_push_eq
-
-@[simp] theorem get!_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]! := by
-  simp [getElem!_def, get!, getD]
-  split <;> rename_i h
-  · simp [getElem?_eq_getElem h]
-    rfl
-  · simp [getElem?_eq_none_iff.2 (by simpa using h)]
+    simp [get_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
 
 end Array
 
@@ -85,6 +74,13 @@ We prefer to pull `List.toArray` outwards.
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
 
+@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
+
+@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
+    a.toArray[i] = a[i]'(by simpa using h) := rfl
+
+@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
+
 @[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
   apply ext'
   simp
@@ -94,14 +90,6 @@ We prefer to pull `List.toArray` outwards.
   funext a
   simp
 
-@[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
-  cases l <;> simp
-
-@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
-
-@[simp] theorem back_toArray [Inhabited α] (l : List α) : l.toArray.back = l.getLast! := by
-  simp only [back, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
-
 theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
     l.toArray.foldrM f init = l.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList]
@@ -159,9 +147,6 @@ namespace Array
 
 @[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
 
--- This is a duplicate of `List.toArray_toList`.
--- It's confusing to guess which namespace this theorem should live in,
--- so we provide both.
 @[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
 
 @[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl
@@ -263,7 +248,7 @@ theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by si
 @[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
 
 theorem getElem?_lt
-    (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i] := dif_pos h
+    (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some (a[i]) := dif_pos h
 
 theorem getElem?_ge
     (a : Array α) {i : Nat} (h : i ≥ a.size) : a[i]? = none := dif_neg (Nat.not_lt_of_le h)
@@ -286,10 +271,8 @@ theorem getD_get? (a : Array α) (i : Nat) (d : α) :
 
 theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
 
-@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) :
-    a.get! i = (a.get? i).getD default := by
-  by_cases p : i < a.size <;>
-  simp only [get!_eq_getD, getD_eq_get?, getD_get?, p, get?_eq_getElem?]
+@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) : a.get! i = (a.get? i).getD default := by
+  by_cases p : i < a.size <;> simp [getD_get?, get!_eq_getD, p]
 
 /-! # set -/
 
@@ -369,8 +352,8 @@ theorem getElem_ofFn_go (f : Fin n → α) (i) {acc k}
     simp only [dif_pos hin]
     rw [getElem_ofFn_go f (i+1) _ hin (by simp [*]) (fun j hj => ?hacc)]
     cases (Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ (by simpa using hj)) with
-    | inl hj => simp [getElem_push, hj, hacc j hj]
-    | inr hj => simp [getElem_push, *]
+    | inl hj => simp [get_push, hj, hacc j hj]
+    | inr hj => simp [get_push, *]
   else
     simp [hin, hacc k (Nat.lt_of_lt_of_le hki (Nat.le_of_not_lt (hi ▸ hin)))]
 termination_by n - i
@@ -438,7 +421,7 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
     idx < a.size :=
   hidx
 
-@[simp] theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
+theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
   erw [Array.mem_def, getElem_eq_getElem_toList]
   apply List.get_mem
 
@@ -447,11 +430,9 @@ theorem getElem_fin_eq_getElem_toList (a : Array α) (i : Fin a.size) : a[i] = a
 @[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
   a[i] = a[i.toNat] := rfl
 
-theorem getElem?_size_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
+theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
   simp [getElem?_neg, h]
 
-@[deprecated getElem?_size_le (since := "2024-10-21")] abbrev get?_len_le := @getElem?_size_le
-
 theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList := by
   simp only [getElem_eq_getElem_toList, List.getElem_mem]
 
@@ -459,39 +440,35 @@ theorem get?_eq_get?_toList (a : Array α) (i : Nat) : a.get? i = a.toList.get?
   simp [getElem?_eq_getElem?_toList]
 
 theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
-  simp only [get!_eq_getElem?, get?_eq_getElem?]
+  simp [get!_eq_getD]
 
 theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < as.size, as[n] = a := by
   cases as
   simp [List.getElem?_eq_some_iff]
 
 @[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
-  simp only [back, get!_eq_getElem?, get?_eq_getElem?, back?]
+  simp [back, back?]
 
 @[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
   simp [back?, getElem?_eq_getElem?_toList]
 
 theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
 
-theorem getElem?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
+theorem get?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     (a.push x)[i]? = some a[i] := by
-  rw [getElem?_pos, getElem_push_lt]
+  rw [getElem?_pos, get_push_lt]
 
-@[deprecated getElem?_push_lt (since := "2024-10-21")] abbrev get?_push_lt := @getElem?_push_lt
+theorem get?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
+  rw [getElem?_pos, get_push_eq]
 
-theorem getElem?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
-  rw [getElem?_pos, getElem_push_eq]
-
-@[deprecated getElem?_push_eq (since := "2024-10-21")] abbrev get?_push_eq := @getElem?_push_eq
-
-theorem getElem?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
+theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
   match Nat.lt_trichotomy i a.size with
   | Or.inl g =>
     have h1 : i < a.size + 1 := by omega
     have h2 : i ≠ a.size := by omega
-    simp [getElem?_def, size_push, g, h1, h2, getElem_push_lt]
+    simp [getElem?_def, size_push, g, h1, h2, get_push_lt]
   | Or.inr (Or.inl heq) =>
-    simp [heq, getElem?_pos, getElem_push_eq]
+    simp [heq, getElem?_pos, get_push_eq]
   | Or.inr (Or.inr g) =>
     simp only [getElem?_def, size_push]
     have h1 : ¬ (i < a.size) := by omega
@@ -499,13 +476,9 @@ theorem getElem?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some
     have h3 : i ≠ a.size := by omega
     simp [h1, h2, h3]
 
-@[deprecated getElem?_push (since := "2024-10-21")] abbrev get?_push := @getElem?_push
-
-@[simp] theorem getElem?_size {a : Array α} : a[a.size]? = none := by
+@[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
   simp only [getElem?_def, Nat.lt_irrefl, dite_false]
 
-@[deprecated getElem?_size (since := "2024-10-21")] abbrev get?_size := @getElem?_size
-
 @[simp] theorem toList_set (a : Array α) (i v) : (a.set i v).toList = a.toList.set i.1 v := rfl
 
 theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
@@ -555,9 +528,6 @@ theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)
 @[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
     a.swapAt i v = (a[i.1], a.set i v) := rfl
 
-@[simp] theorem size_swapAt (a : Array α) (i : Fin a.size) (v : α) :
-    (a.swapAt i v).2.size = a.size := by simp [swapAt_def]
-
 @[simp]
 theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
     a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
@@ -590,11 +560,11 @@ theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.
   · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
   · intros i h h'
     if hlt : i < as.pop.size then
-      rw [getElem_push_lt (h:=hlt), getElem_pop]
+      rw [get_push_lt (h:=hlt), getElem_pop]
     else
       have heq : i = as.pop.size :=
         Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
-      cases heq; rw [getElem_push_eq, back, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl
+      cases heq; rw [get_push_eq, back, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl
 
 theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
     ∃ (bs : Array α) (c : α), as = bs.push c :=
@@ -803,9 +773,9 @@ theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h
     · intro j h
       simp at h ⊢
       by_cases h' : j < size b
-      · rw [getElem_push]
+      · rw [get_push]
         simp_all
-      · rw [getElem_push, dif_neg h']
+      · rw [get_push, dif_neg h']
         simp only [show j = i by omega]
         exact (hs _ m).1
 
@@ -830,7 +800,7 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
     (as.push x).map f = (as.map f).push (f x) := by
   ext
   · simp
-  · simp only [getElem_map, getElem_push, size_map]
+  · simp only [getElem_map, get_push, size_map]
     split <;> rfl
 
 @[simp] theorem map_pop {f : α → β} {as : Array α} :
@@ -852,12 +822,6 @@ theorem getElem_modify {as : Array α} {x i} (h : i < (as.modify x f).size) :
   · simp only [Id.bind_eq, get_set _ _ _ (by simpa using h)]; split <;> simp [*]
   · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
 
-@[simp] theorem toList_modify (as : Array α) (f : α → α) :
-    (as.modify x f).toList = as.toList.modify f x := by
-  apply List.ext_getElem
-  · simp
-  · simp [getElem_modify, List.getElem_modify]
-
 theorem getElem_modify_self {as : Array α} {i : Nat} (f : α → α) (h : i < (as.modify i f).size) :
     (as.modify i f)[i] = f (as[i]'(by simpa using h)) := by
   simp [getElem_modify h]
@@ -867,11 +831,6 @@ theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
     (as.modify i f)[j] = as[j]'(by simpa using hj) := by
   simp [getElem_modify hj, h]
 
-theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} :
-    (as.modify i f)[j]? = if i = j then as[j]?.map f else as[j]? := by
-  simp only [getElem?_def, size_modify, getElem_modify, Option.map_dif]
-  split <;> split <;> rfl
-
 /-! ### filter -/
 
 @[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
@@ -933,7 +892,7 @@ theorem filterMap_congr {as bs : Array α} (h : as = bs)
 
 theorem size_empty : (#[] : Array α).size = 0 := rfl
 
-@[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
+theorem toList_empty : (#[] : Array α).toList = [] := rfl
 
 /-! ### append -/
 
@@ -1091,7 +1050,7 @@ theorem getElem_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i
       have h₂ : bs.size < (extract.loop as size (start+1) (bs.push as[start])).size := by
         rw [size_extract_loop]; apply Nat.lt_of_lt_of_le h₁; exact Nat.le_add_right ..
       have h : (extract.loop as size (start + 1) (push bs as[start]))[bs.size] = as[start] := by
-        rw [getElem_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, getElem_push_eq]
+        rw [getElem_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
       rw [h]; congr; rw [Nat.add_sub_cancel]
     else
       have hge : bs.size + 1 ≤ i := Nat.lt_of_le_of_ne hge hi
@@ -1118,14 +1077,6 @@ theorem getElem?_extract {as : Array α} {start stop : Nat} :
     · omega
   · rfl
 
-@[simp] theorem toList_extract (as : Array α) (start stop : Nat) :
-    (as.extract start stop).toList = (as.toList.drop start).take (stop - start) := by
-  apply List.ext_getElem
-  · simp only [length_toList, size_extract, List.length_take, List.length_drop]
-    omega
-  · intros n h₁ h₂
-    simp
-
 @[simp] theorem extract_all (as : Array α) : as.extract 0 as.size = as := by
   apply ext
   · rw [size_extract, Nat.min_self, Nat.sub_zero]
@@ -1295,7 +1246,7 @@ open Fin
       · assumption
 
 theorem getElem_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < a.size) :
-    (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i] else a[k] := by
+    (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i]  else a[k] := by
   split
   · simp_all only [getElem_swap_left]
   · split <;> simp_all
@@ -1305,7 +1256,7 @@ theorem getElem_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < (a.sw
   apply getElem_swap'
 
 @[simp] theorem swap_swap (a : Array α) {i j : Fin a.size} :
-    (a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸ i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸ j.2⟩ = a := by
+    (a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸j.2⟩ = a := by
   apply ext
   · simp only [size_swap]
   · intros
@@ -1440,11 +1391,6 @@ theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p
   apply ext'
   simp
 
-@[simp] theorem modify_toArray (f : α → α) (l : List α) :
-    l.toArray.modify i f = (l.modify f i).toArray := by
-  apply ext'
-  simp
-
 @[simp] theorem filter_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
     l.toArray.filter p 0 stop = (l.filter p).toArray := by
   subst h
@@ -1473,11 +1419,6 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
   apply ext'
   simp
 
-@[simp] theorem toArray_extract (l : List α) (start stop : Nat) :
-    l.toArray.extract start stop = ((l.drop start).take (stop - start)).toArray := by
-  apply ext'
-  simp
-
 end List
 
 /-! ### Deprecations -/

src/Init/Data/Array/MapIdx.lean

@@ -9,84 +9,56 @@ import Init.Data.List.MapIdx
 
 namespace Array
 
-/-! ### mapFinIdx -/
+
+/-! ### mapIdx -/
 
 -- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
-theorem mapFinIdx_induction (as : Array α) (f : Fin as.size → α → β)
+theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
     (motive : Nat → Prop) (h0 : motive 0)
     (p : Fin as.size → β → Prop)
     (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
-    motive as.size ∧ ∃ eq : (Array.mapFinIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapFinIdx as f)[i]) := by
+    motive as.size ∧ ∃ eq : (Array.mapIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) := by
   let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
-    let arr : Array β := Array.mapFinIdxM.map (m := Id) as f i j h bs
+    let arr : Array β := Array.mapIdxM.map (m := Id) as f i j h bs
     motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by
-    induction i generalizing j bs with simp [mapFinIdxM.map]
+    induction i generalizing j bs with simp [mapIdxM.map]
     | zero =>
       have := (Nat.zero_add _).symm.trans h
       exact ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩
     | succ i ih =>
       apply @ih (bs.push (f ⟨j, by omega⟩ as[j])) (j + 1) (by omega) (by simp; omega)
       · intro i i_lt h'
-        rw [getElem_push]
+        rw [get_push]
         split
         · apply h₂
         · simp only [size_push] at h'
           obtain rfl : i = j := by omega
           apply (hs ⟨i, by omega⟩ hm).1
       · exact (hs ⟨j, by omega⟩ hm).2
-  simp [mapFinIdx, mapFinIdxM]; exact go rfl nofun h0
+  simp [mapIdx, mapIdxM]; exact go rfl nofun h0
 
-theorem mapFinIdx_spec (as : Array α) (f : Fin as.size → α → β)
-    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
-    ∃ eq : (Array.mapFinIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapFinIdx as f)[i]) :=
-  (mapFinIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
-
-@[simp] theorem size_mapFinIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapFinIdx f).size = a.size :=
-  (mapFinIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
-
-@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
-  Array.size_mapFinIdx _ _
-
-@[simp] theorem getElem_mapFinIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
-    (h : i < (mapFinIdx a f).size) :
-    (a.mapFinIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
-  (mapFinIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
-
-@[simp] theorem getElem?_mapFinIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
-    (a.mapFinIdx f)[i]? =
-      a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
-  simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
-  split <;> simp_all
-
-/-! ### mapIdx -/
-
-theorem mapIdx_induction (as : Array α) (f : Nat → α → β)
-    (motive : Nat → Prop) (h0 : motive 0)
-    (p : Fin as.size → β → Prop)
-    (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
-    motive as.size ∧ ∃ eq : (Array.mapIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
-  mapFinIdx_induction as (fun i a => f i a) motive h0 p hs
-
-theorem mapIdx_spec (as : Array α) (f : Nat → α → β)
+theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
     (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
     ∃ eq : (Array.mapIdx as f).size = as.size,
       ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
   (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
 
-@[simp] theorem size_mapIdx (a : Array α) (f : Nat → α → β) : (a.mapIdx f).size = a.size :=
+@[simp] theorem size_mapIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapIdx f).size = a.size :=
   (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
 
-@[simp] theorem getElem_mapIdx (a : Array α) (f : Nat → α → β) (i : Nat)
-    (h : i < (mapIdx a f).size) :
-    (a.mapIdx f)[i] = f i (a[i]'(by simp_all)) :=
-  (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i (by simp_all)
+@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
+  Array.size_mapIdx _ _
 
-@[simp] theorem getElem?_mapIdx (a : Array α) (f : Nat → α → β) (i : Nat) :
+@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
+    (h : i < (mapIdx a f).size) :
+    (a.mapIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
+  (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
+
+@[simp] theorem getElem?_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
     (a.mapIdx f)[i]? =
-      a[i]?.map (f i) := by
-  simp [getElem?_def, size_mapIdx, getElem_mapIdx]
+      a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
+  simp only [getElem?_def, size_mapIdx, getElem_mapIdx]
+  split <;> simp_all
 
 end Array

src/Init/Data/BitVec/Lemmas.lean

@@ -316,12 +316,6 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
   simp [Nat.sub_sub_eq_min, Nat.min_eq_right]
   omega
 
-@[simp] theorem sub_add_bmod_cancel {x y : BitVec w} :
-    ((((2 ^ w : Nat) - y.toNat) : Int) + x.toNat).bmod (2 ^ w) =
-      ((x.toNat : Int) - y.toNat).bmod (2 ^ w) := by
-  rw [Int.sub_eq_add_neg, Int.add_assoc, Int.add_comm, Int.bmod_add_cancel, Int.add_comm,
-    Int.sub_eq_add_neg]
-
 private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
   Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
 
@@ -1980,10 +1974,6 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN
 @[simp] theorem toNat_sub {n} (x y : BitVec n) :
     (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
 
-@[simp, bv_toNat] theorem toInt_sub {x y : BitVec w} :
-    (x - y).toInt = (x.toInt - y.toInt).bmod (2 ^ w) := by
-  simp [toInt_eq_toNat_bmod, @Int.ofNat_sub y.toNat (2 ^ w) (by omega)]
-
 -- We prefer this lemma to `toNat_sub` for the `bv_toNat` simp set.
 -- For reasons we don't yet understand, unfolding via `toNat_sub` sometimes
 -- results in `omega` generating proof terms that are very slow in the kernel.
@@ -2006,8 +1996,6 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
 
 @[simp] protected theorem sub_zero (x : BitVec n) : x - 0#n = x := by apply eq_of_toNat_eq ; simp
 
-@[simp] protected theorem zero_sub (x : BitVec n) : 0#n - x = -x := rfl
-
 @[simp] protected theorem sub_self (x : BitVec n) : x - x = 0#n := by
   apply eq_of_toNat_eq
   simp only [toNat_sub]
@@ -2020,8 +2008,18 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
 
 theorem toInt_neg {x : BitVec w} :
     (-x).toInt = (-x.toInt).bmod (2 ^ w) := by
-  rw [← BitVec.zero_sub, toInt_sub]
-  simp [BitVec.toInt_ofNat]
+  simp only [toInt_eq_toNat_bmod, toNat_neg, Int.ofNat_emod, Int.emod_bmod_congr]
+  rw [← Int.subNatNat_of_le (by omega), Int.subNatNat_eq_coe, Int.sub_eq_add_neg, Int.add_comm,
+    Int.bmod_add_cancel]
+  by_cases h : x.toNat < ((2 ^ w) + 1) / 2
+  · rw [Int.bmod_pos (x := x.toNat)]
+    all_goals simp only [toNat_mod_cancel']
+    norm_cast
+  · rw [Int.bmod_neg (x := x.toNat)]
+    · simp only [toNat_mod_cancel']
+      rw_mod_cast [Int.neg_sub, Int.sub_eq_add_neg, Int.add_comm, Int.bmod_add_cancel]
+    · norm_cast
+      simp_all
 
 @[simp] theorem toFin_neg (x : BitVec n) :
     (-x).toFin = Fin.ofNat' (2^n) (2^n - x.toNat) :=

src/Init/Data/Int/DivModLemmas.lean

@@ -1125,17 +1125,6 @@ theorem emod_add_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n + y) n = Int.bmo
   simp [Int.emod_def, Int.sub_eq_add_neg]
   rw [←Int.mul_neg, Int.add_right_comm,  Int.bmod_add_mul_cancel]
 
-@[simp]
-theorem emod_sub_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n - y) n = Int.bmod (x - y) n := by
-  simp only [emod_def, Int.sub_eq_add_neg]
-  rw [←Int.mul_neg, Int.add_right_comm,  Int.bmod_add_mul_cancel]
-
-@[simp]
-theorem sub_emod_bmod_congr (x : Int) (n : Nat) : Int.bmod (x - y%n) n = Int.bmod (x - y) n := by
-  simp only [emod_def]
-  rw [Int.sub_eq_add_neg, Int.neg_sub, Int.sub_eq_add_neg, ← Int.add_assoc, Int.add_right_comm,
-    Int.bmod_add_mul_cancel, Int.sub_eq_add_neg]
-
 @[simp]
 theorem emod_mul_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n * y) n = Int.bmod (x * y) n := by
   simp [Int.emod_def, Int.sub_eq_add_neg]
@@ -1151,28 +1140,9 @@ theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n
     rw [Int.sub_eq_add_neg, Int.add_right_comm, ←Int.sub_eq_add_neg]
     simp
 
-@[simp]
-theorem bmod_sub_bmod_congr : Int.bmod (Int.bmod x n - y) n = Int.bmod (x - y) n := by
-  rw [Int.bmod_def x n]
-  split
-  next p =>
-    simp only [emod_sub_bmod_congr]
-  next p =>
-    rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.add_right_comm, ←Int.sub_eq_add_neg, ← Int.sub_eq_add_neg]
-    simp [emod_sub_bmod_congr]
-
 @[simp] theorem add_bmod_bmod : Int.bmod (x + Int.bmod y n) n = Int.bmod (x + y) n := by
   rw [Int.add_comm x, Int.bmod_add_bmod_congr, Int.add_comm y]
 
-@[simp] theorem sub_bmod_bmod : Int.bmod (x - Int.bmod y n) n = Int.bmod (x - y) n := by
-  rw [Int.bmod_def y n]
-  split
-  next p =>
-    simp [sub_emod_bmod_congr]
-  next p =>
-    rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.neg_add, Int.neg_neg, ← Int.add_assoc, ← Int.sub_eq_add_neg]
-    simp [sub_emod_bmod_congr]
-
 @[simp]
 theorem bmod_mul_bmod : Int.bmod (Int.bmod x n * y) n = Int.bmod (x * y) n := by
   rw [bmod_def x n]

src/Init/Data/List/Basic.lean

@@ -38,7 +38,7 @@ The operations are organized as follow:
 * Sublists: `take`, `drop`, `takeWhile`, `dropWhile`, `partition`, `dropLast`,
   `isPrefixOf`, `isPrefixOf?`, `isSuffixOf`, `isSuffixOf?`, `Subset`, `Sublist`,
   `rotateLeft` and `rotateRight`.
-* Manipulating elements: `replace`, `insert`, `modify`, `erase`, `eraseP`, `eraseIdx`.
+* Manipulating elements: `replace`, `insert`, `erase`, `eraseP`, `eraseIdx`.
 * Finding elements: `find?`, `findSome?`, `findIdx`, `indexOf`, `findIdx?`, `indexOf?`,
  `countP`, `count`, and `lookup`.
 * Logic: `any`, `all`, `or`, and `and`.
@@ -122,11 +122,6 @@ protected def beq [BEq α] : List α → List α → Bool
   | a::as, b::bs => a == b && List.beq as bs
   | _,     _     => false
 
-@[simp] theorem beq_nil_nil [BEq α] : List.beq ([] : List α) ([] : List α) = true := rfl
-@[simp] theorem beq_cons_nil [BEq α] (a : α) (as : List α) : List.beq (a::as) [] = false := rfl
-@[simp] theorem beq_nil_cons [BEq α] (a : α) (as : List α) : List.beq [] (a::as) = false := rfl
-theorem beq_cons₂ [BEq α] (a b : α) (as bs : List α) : List.beq (a::as) (b::bs) = (a == b && List.beq as bs) := rfl
-
 instance [BEq α] : BEq (List α) := ⟨List.beq⟩
 
 instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where
@@ -1119,35 +1114,6 @@ theorem replace_cons [BEq α] {a : α} :
 @[inline] protected def insert [BEq α] (a : α) (l : List α) : List α :=
   if l.elem a then l else a :: l
 
-/-! ### modify -/
-
-/--
-Apply a function to the nth tail of `l`. Returns the input without
-using `f` if the index is larger than the length of the List.
-```
-modifyTailIdx f 2 [a, b, c] = [a, b] ++ f [c]
-```
--/
-@[simp] def modifyTailIdx (f : List α → List α) : Nat → List α → List α
-  | 0, l => f l
-  | _+1, [] => []
-  | n+1, a :: l => a :: modifyTailIdx f n l
-
-/-- Apply `f` to the head of the list, if it exists. -/
-@[inline] def modifyHead (f : α → α) : List α → List α
-  | [] => []
-  | a :: l => f a :: l
-
-@[simp] theorem modifyHead_nil (f : α → α) : [].modifyHead f = [] := by rw [modifyHead]
-@[simp] theorem modifyHead_cons (a : α) (l : List α) (f : α → α) :
-    (a :: l).modifyHead f = f a :: l := by rw [modifyHead]
-
-/--
-Apply `f` to the nth element of the list, if it exists, replacing that element with the result.
--/
-def modify (f : α → α) : Nat → List α → List α :=
-  modifyTailIdx (modifyHead f)
-
 /-! ### erase -/
 
 /--
@@ -1452,15 +1418,11 @@ def sum {α} [Add α] [Zero α] : List α → α :=
 @[simp] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
 
 /-- Sum of a list of natural numbers. -/
-@[deprecated List.sum (since := "2024-10-17")]
+-- We intend to subsequently deprecate this in favor of `List.sum`.
 protected def _root_.Nat.sum (l : List Nat) : Nat := l.foldr (·+·) 0
 
-set_option linter.deprecated false in
-@[simp, deprecated sum_nil (since := "2024-10-17")]
-theorem _root_.Nat.sum_nil : Nat.sum ([] : List Nat) = 0 := rfl
-set_option linter.deprecated false in
-@[simp, deprecated sum_cons (since := "2024-10-17")]
-theorem _root_.Nat.sum_cons (a : Nat) (l : List Nat) :
+@[simp] theorem _root_.Nat.sum_nil : Nat.sum ([] : List Nat) = 0 := rfl
+@[simp] theorem _root_.Nat.sum_cons (a : Nat) (l : List Nat) :
     Nat.sum (a::l) = a + Nat.sum l := rfl
 
 /-! ### range -/

src/Init/Data/List/Impl.lean

@@ -38,7 +38,7 @@ The following operations were already given `@[csimp]` replacements in `Init/Dat
 
 The following operations are given `@[csimp]` replacements below:
 `set`, `filterMap`, `foldr`, `append`, `bind`, `join`,
-`take`, `takeWhile`, `dropLast`, `replace`, `modify`, `erase`, `eraseIdx`, `zipWith`,
+`take`, `takeWhile`, `dropLast`, `replace`, `erase`, `eraseIdx`, `zipWith`,
 `enumFrom`, and `intercalate`.
 
 -/
@@ -197,24 +197,6 @@ The following operations are given `@[csimp]` replacements below:
     · simp [*]
     · intro h; rw [IH] <;> simp_all
 
-/-! ### modify -/
-
-/-- Tail-recursive version of `modify`. -/
-def modifyTR (f : α → α) (n : Nat) (l : List α) : List α := go l n #[] where
-  /-- Auxiliary for `modifyTR`: `modifyTR.go f l n acc = acc.toList ++ modify f n l`. -/
-  go : List α → Nat → Array α → List α
-  | [], _, acc => acc.toList
-  | a :: l, 0, acc => acc.toListAppend (f a :: l)
-  | a :: l, n+1, acc => go l n (acc.push a)
-
-theorem modifyTR_go_eq : ∀ l n, modifyTR.go f l n acc = acc.toList ++ modify f n l
-  | [], n => by cases n <;> simp [modifyTR.go, modify]
-  | a :: l, 0 => by simp [modifyTR.go, modify]
-  | a :: l, n+1 => by simp [modifyTR.go, modify, modifyTR_go_eq l]
-
-@[csimp] theorem modify_eq_modifyTR : @modify = @modifyTR := by
-  funext α f n l; simp [modifyTR, modifyTR_go_eq]
-
 /-! ### erase -/
 
 /-- Tail recursive version of `List.erase`. -/

src/Init/Data/List/Lemmas.lean

@@ -1047,6 +1047,9 @@ theorem get_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length) :
 
 @[simp] theorem getLast?_singleton (a : α) : getLast? [a] = a := rfl
 
+theorem getLast!_of_getLast? [Inhabited α] : ∀ {l : List α}, getLast? l = some a → getLast! l = a
+  | _ :: _, rfl => rfl
+
 theorem getLast?_eq_getLast : ∀ l h, @getLast? α l = some (getLast l h)
   | [], h => nomatch h rfl
   | _ :: _, _ => rfl
@@ -1080,21 +1083,6 @@ theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by
 theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by
   rw [getLastD_eq_getLast?, getLast?_concat]; rfl
 
-/-! ### getLast! -/
-
-@[simp] theorem getLast!_nil [Inhabited α] : ([] : List α).getLast! = default := rfl
-
-theorem getLast!_of_getLast? [Inhabited α] : ∀ {l : List α}, getLast? l = some a → getLast! l = a
-  | _ :: _, rfl => rfl
-
-theorem getLast!_eq_getElem! [Inhabited α] {l : List α} : l.getLast! = l[l.length - 1]! := by
-  cases l with
-  | nil => simp
-  | cons _ _ =>
-    apply getLast!_of_getLast?
-    rw [getElem!_pos, getElem_cons_length (h := by simp)]
-    rfl
-
 /-! ## Head and tail -/
 
 /-! ### head -/

src/Init/Data/List/Nat.lean

@@ -12,5 +12,3 @@ import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Count
 import Init.Data.List.Nat.Erase
 import Init.Data.List.Nat.Find
-import Init.Data.List.Nat.BEq
-import Init.Data.List.Nat.Modify

src/Init/Data/List/Nat/BEq.lean

@@ -1,47 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-prelude
-import Init.Data.Nat.Lemmas
-import Init.Data.List.Basic
-
-namespace List
-
-/-! ### isEqv-/
-
-theorem isEqv_eq_decide (a b : List α) (r) :
-    isEqv a b r = if h : a.length = b.length then
-      decide (∀ (i : Nat) (h' : i < a.length), r (a[i]'(h ▸ h')) (b[i]'(h ▸ h'))) else false := by
-  induction a generalizing b with
-  | nil =>
-    cases b <;> simp
-  | cons a as ih =>
-    cases b with
-    | nil => simp
-    | cons b bs =>
-      simp only [isEqv, ih, length_cons, Nat.add_right_cancel_iff]
-      split <;> simp [Nat.forall_lt_succ_left']
-
-/-! ### beq -/
-
-theorem beq_eq_isEqv [BEq α] (a b : List α) : a.beq b = isEqv a b (· == ·) := by
-  induction a generalizing b with
-  | nil =>
-    cases b <;> simp
-  | cons a as ih =>
-    cases b with
-    | nil => simp
-    | cons b bs =>
-      simp only [beq_cons₂, ih, isEqv_eq_decide, length_cons, Nat.add_right_cancel_iff,
-        Nat.forall_lt_succ_left', getElem_cons_zero, getElem_cons_succ, Bool.decide_and,
-        Bool.decide_eq_true]
-      split <;> simp
-
-theorem beq_eq_decide [BEq α] (a b : List α) :
-    (a == b) = if h : a.length = b.length then
-      decide (∀ (i : Nat) (h' : i < a.length), a[i] == b[i]'(h ▸ h')) else false := by
-  simp [BEq.beq, beq_eq_isEqv, isEqv_eq_decide]
-
-end List

src/Init/Data/List/Nat/Modify.lean

@@ -1,102 +0,0 @@
-/-
-Copyright (c) 2014 Parikshit Khanna. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
--/
-
-prelude
-import Init.Data.List.Nat.TakeDrop
-
-namespace List
-
-/-! ### modifyHead -/
-
-@[simp] theorem modifyHead_modifyHead (l : List α) (f g : α → α) :
-    (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp [modifyHead]
-
-/-! ### modify -/
-
-@[simp] theorem modify_nil (f : α → α) (n) : [].modify f n = [] := by cases n <;> rfl
-
-@[simp] theorem modify_zero_cons (f : α → α) (a : α) (l : List α) :
-    (a :: l).modify f 0 = f a :: l := rfl
-
-@[simp] theorem modify_succ_cons (f : α → α) (a : α) (l : List α) (n) :
-    (a :: l).modify f (n + 1) = a :: l.modify f n := by rfl
-
-theorem modifyTailIdx_id : ∀ n (l : List α), l.modifyTailIdx id n = l
-  | 0, _ => rfl
-  | _+1, [] => rfl
-  | n+1, a :: l => congrArg (cons a) (modifyTailIdx_id n l)
-
-theorem eraseIdx_eq_modifyTailIdx : ∀ n (l : List α), eraseIdx l n = modifyTailIdx tail n l
-  | 0, l => by cases l <;> rfl
-  | _+1, [] => rfl
-  | _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyTailIdx _ _)
-
-theorem getElem?_modify (f : α → α) :
-    ∀ n (l : List α) m, (modify f n l)[m]? = (fun a => if n = m then f a else a) <$> l[m]?
-  | n, l, 0 => by cases l <;> cases n <;> simp
-  | n, [], _+1 => by cases n <;> rfl
-  | 0, _ :: l, m+1 => by cases h : l[m]? <;> simp [h, modify, m.succ_ne_zero.symm]
-  | n+1, a :: l, m+1 => by
-    simp only [modify_succ_cons, getElem?_cons_succ, Nat.reduceEqDiff, Option.map_eq_map]
-    refine (getElem?_modify f n l m).trans ?_
-    cases h' : l[m]? <;> by_cases h : n = m <;>
-      simp [h, if_pos, if_neg, Option.map, mt Nat.succ.inj, not_false_iff, h']
-
-@[simp] theorem length_modifyTailIdx (f : List α → List α) (H : ∀ l, length (f l) = length l) :
-    ∀ n l, length (modifyTailIdx f n l) = length l
-  | 0, _ => H _
-  | _+1, [] => rfl
-  | _+1, _ :: _ => congrArg (·+1) (length_modifyTailIdx _ H _ _)
-
-theorem modifyTailIdx_add (f : List α → List α) (n) (l₁ l₂ : List α) :
-    modifyTailIdx f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ modifyTailIdx f n l₂ := by
-  induction l₁ <;> simp [*, Nat.succ_add]
-
-@[simp] theorem length_modify (f : α → α) : ∀ n l, length (modify f n l) = length l :=
-  length_modifyTailIdx _ fun l => by cases l <;> rfl
-
-@[simp] theorem getElem?_modify_eq (f : α → α) (n) (l : List α) :
-    (modify f n l)[n]? = f <$> l[n]? := by
-  simp only [getElem?_modify, if_pos]
-
-@[simp] theorem getElem?_modify_ne (f : α → α) {m n} (l : List α) (h : m ≠ n) :
-    (modify f m l)[n]? = l[n]? := by
-  simp only [getElem?_modify, if_neg h, id_map']
-
-theorem getElem_modify (f : α → α) (n) (l : List α) (m) (h : m < (modify f n l).length) :
-    (modify f n l)[m] =
-      if n = m then f (l[m]'(by simp at h; omega)) else l[m]'(by simp at h; omega) := by
-  rw [getElem_eq_iff, getElem?_modify]
-  simp at h
-  simp [h]
-
-theorem modifyTailIdx_eq_take_drop (f : List α → List α) (H : f [] = []) :
-    ∀ n l, modifyTailIdx f n l = take n l ++ f (drop n l)
-  | 0, _ => rfl
-  | _ + 1, [] => H.symm
-  | n + 1, b :: l => congrArg (cons b) (modifyTailIdx_eq_take_drop f H n l)
-
-theorem modify_eq_take_drop (f : α → α) :
-    ∀ n l, modify f n l = take n l ++ modifyHead f (drop n l) :=
-  modifyTailIdx_eq_take_drop _ rfl
-
-theorem modify_eq_take_cons_drop (f : α → α) {n l} (h : n < length l) :
-    modify f n l = take n l ++ f l[n] :: drop (n + 1) l := by
-  rw [modify_eq_take_drop, drop_eq_getElem_cons h]; rfl
-
-theorem exists_of_modifyTailIdx (f : List α → List α) {n} {l : List α} (h : n ≤ l.length) :
-    ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n ∧ modifyTailIdx f n l = l₁ ++ f l₂ :=
-  have ⟨_, _, eq, hl⟩ : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n :=
-    ⟨_, _, (take_append_drop n l).symm, length_take_of_le h⟩
-  ⟨_, _, eq, hl, hl ▸ eq ▸ modifyTailIdx_add (n := 0) ..⟩
-
-theorem exists_of_modify (f : α → α) {n} {l : List α} (h : n < l.length) :
-    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = n ∧ modify f n l = l₁ ++ f a :: l₂ :=
-  match exists_of_modifyTailIdx _ (Nat.le_of_lt h) with
-  | ⟨_, _::_, eq, hl, H⟩ => ⟨_, _, _, eq, hl, H⟩
-  | ⟨_, [], eq, hl, _⟩ => nomatch Nat.ne_of_gt h (eq ▸ append_nil _ ▸ hl)
-
-end List

src/Init/Data/Nat/Lemmas.lean

@@ -32,77 +32,6 @@ namespace Nat
 @[simp] theorem exists_add_one_eq : (∃ n, n + 1 = a) ↔ 0 < a :=
   ⟨fun ⟨n, h⟩ => by omega, fun h => ⟨a - 1, by omega⟩⟩
 
-/-- Dependent variant of `forall_lt_succ_right`. -/
-theorem forall_lt_succ_right' {p : (m : Nat) → (m < n + 1) → Prop} :
-    (∀ m (h : m < n + 1), p m h) ↔ (∀ m (h : m < n), p m (by omega)) ∧ p n (by omega) := by
-  simp only [Nat.lt_succ_iff, Nat.le_iff_lt_or_eq]
-  constructor
-  · intro w
-    constructor
-    · intro m h
-      exact w _ (.inl h)
-    · exact w _ (.inr rfl)
-  · rintro w m (h|rfl)
-    · exact w.1 _ h
-    · exact w.2
-
-/-- See `forall_lt_succ_right'` for a variant where `p` takes the bound as an argument. -/
-theorem forall_lt_succ_right {p : Nat → Prop} :
-    (∀ m, m < n + 1 → p m) ↔ (∀ m, m < n → p m) ∧ p n := by
-  simpa using forall_lt_succ_right' (p := fun m _ => p m)
-
-/-- Dependent variant of `forall_lt_succ_left`. -/
-theorem forall_lt_succ_left' {p : (m : Nat) → (m < n + 1) → Prop} :
-    (∀ m (h : m < n + 1), p m h) ↔ p 0 (by omega) ∧ (∀ m (h : m < n), p (m + 1) (by omega)) := by
-  constructor
-  · intro w
-    constructor
-    · exact w 0 (by omega)
-    · intro m h
-      exact w (m + 1) (by omega)
-  · rintro ⟨h₀, h₁⟩ m h
-    cases m with
-    | zero => exact h₀
-    | succ m => exact h₁ m (by omega)
-
-/-- See `forall_lt_succ_left'` for a variant where `p` takes the bound as an argument. -/
-theorem forall_lt_succ_left {p : Nat → Prop} :
-    (∀ m, m < n + 1 → p m) ↔ p 0 ∧ (∀ m, m < n → p (m + 1)) := by
-  simpa using forall_lt_succ_left' (p := fun m _ => p m)
-
-/-- Dependent variant of `exists_lt_succ_right`. -/
-theorem exists_lt_succ_right' {p : (m : Nat) → (m < n + 1) → Prop} :
-    (∃ m, ∃ (h : m < n + 1), p m h) ↔ (∃ m, ∃ (h : m < n), p m (by omega)) ∨ p n (by omega) := by
-  simp only [Nat.lt_succ_iff, Nat.le_iff_lt_or_eq]
-  constructor
-  · rintro ⟨m, (h|rfl), w⟩
-    · exact .inl ⟨m, h, w⟩
-    · exact .inr w
-  · rintro (⟨m, h, w⟩ | w)
-    · exact ⟨m, by omega, w⟩
-    · exact ⟨n, by omega, w⟩
-
-/-- See `exists_lt_succ_right'` for a variant where `p` takes the bound as an argument. -/
-theorem exists_lt_succ_right {p : Nat → Prop} :
-    (∃ m, m < n + 1 ∧ p m) ↔ (∃ m, m < n ∧ p m) ∨ p n := by
-  simpa using exists_lt_succ_right' (p := fun m _ => p m)
-
-/-- Dependent variant of `exists_lt_succ_left`. -/
-theorem exists_lt_succ_left' {p : (m : Nat) → (m < n + 1) → Prop} :
-    (∃ m, ∃ (h : m < n + 1), p m h) ↔ p 0 (by omega) ∨ (∃ m, ∃ (h : m < n), p (m + 1) (by omega)) := by
-  constructor
-  · rintro ⟨_|m, h, w⟩
-    · exact .inl w
-    · exact .inr ⟨m, by omega, w⟩
-  · rintro (w|⟨m, h, w⟩)
-    · exact ⟨0, by omega, w⟩
-    · exact ⟨m + 1, by omega, w⟩
-
-/-- See `exists_lt_succ_left'` for a variant where `p` takes the bound as an argument. -/
-theorem exists_lt_succ_left {p : Nat → Prop} :
-    (∃ m, m < n + 1 ∧ p m) ↔ p 0 ∨ (∃ m, m < n ∧ p (m + 1)) := by
-  simpa using exists_lt_succ_left' (p := fun m _ => p m)
-
 /-! ## add -/
 
 protected theorem add_add_add_comm (a b c d : Nat) : (a + b) + (c + d) = (a + c) + (b + d) := by

src/Init/NotationExtra.lean

@@ -10,7 +10,6 @@ import Init.Data.ToString.Basic
 import Init.Data.Array.Subarray
 import Init.Conv
 import Init.Meta
-import Init.While
 
 namespace Lean
 
@@ -169,9 +168,9 @@ end Lean
   | _                => throw ()
 
 @[app_unexpander sorryAx] def unexpandSorryAx : Lean.PrettyPrinter.Unexpander
-  | `($(_) $_)    => `(sorry)
-  | `($(_) $_ $_) => `(sorry)
-  | _             => throw ()
+  | `($(_) _)   => `(sorry)
+  | `($(_) _ _) => `(sorry)
+  | _           => throw ()
 
 @[app_unexpander Eq.ndrec] def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander
   | `($(_) $m $h) => `($h ▸ $m)
@@ -345,6 +344,42 @@ syntax (name := solveTactic) "solve" withPosition((ppDedent(ppLine) colGe "| " t
 macro_rules
   | `(tactic| solve $[| $ts]* ) => `(tactic| focus first $[| ($ts); done]*)
 
+/-! # `repeat` and `while` notation -/
+
+inductive Loop where
+  | mk
+
+@[inline]
+partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
+  let rec @[specialize] loop (b : β) : m β := do
+    match ← f () b with
+      | ForInStep.done b  => pure b
+      | ForInStep.yield b => loop b
+  loop init
+
+instance : ForIn m Loop Unit where
+  forIn := Loop.forIn
+
+syntax "repeat " doSeq : doElem
+
+macro_rules
+  | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
+
+syntax "while " ident " : " termBeforeDo " do " doSeq : doElem
+
+macro_rules
+  | `(doElem| while $h : $cond do $seq) => `(doElem| repeat if $h : $cond then $seq else break)
+
+syntax "while " termBeforeDo " do " doSeq : doElem
+
+macro_rules
+  | `(doElem| while $cond do $seq) => `(doElem| repeat if $cond then $seq else break)
+
+syntax "repeat " doSeq ppDedent(ppLine) "until " term : doElem
+
+macro_rules
+  | `(doElem| repeat $seq until $cond) => `(doElem| repeat do $seq:doSeq; if $cond then break)
+
 macro:50 e:term:51 " matches " p:sepBy1(term:51, " | ") : term =>
   `(((match $e:term with | $[$p:term]|* => true | _ => false) : Bool))
 

src/Init/While.lean

@@ -1,51 +0,0 @@
-/-
-Copyright (c) 2020 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Core
-
-/-!
-# Notation for `while` and `repeat` loops.
--/
-
-namespace Lean
-
-/-! # `repeat` and `while` notation -/
-
-inductive Loop where
-  | mk
-
-@[inline]
-partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
-  let rec @[specialize] loop (b : β) : m β := do
-    match ← f () b with
-      | ForInStep.done b  => pure b
-      | ForInStep.yield b => loop b
-  loop init
-
-instance : ForIn m Loop Unit where
-  forIn := Loop.forIn
-
-syntax "repeat " doSeq : doElem
-
-macro_rules
-  | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
-
-syntax "while " ident " : " termBeforeDo " do " doSeq : doElem
-
-macro_rules
-  | `(doElem| while $h : $cond do $seq) => `(doElem| repeat if $h : $cond then $seq else break)
-
-syntax "while " termBeforeDo " do " doSeq : doElem
-
-macro_rules
-  | `(doElem| while $cond do $seq) => `(doElem| repeat if $cond then $seq else break)
-
-syntax "repeat " doSeq ppDedent(ppLine) "until " term : doElem
-
-macro_rules
-  | `(doElem| repeat $seq until $cond) => `(doElem| repeat do $seq:doSeq; if $cond then break)
-
-end Lean

src/Lean/Declaration.lean

@@ -369,13 +369,8 @@ def RecursorVal.getFirstIndexIdx (v : RecursorVal) : Nat :=
 def RecursorVal.getFirstMinorIdx (v : RecursorVal) : Nat :=
   v.numParams + v.numMotives
 
-/-- The inductive type of the major argument of the recursor. -/
-def RecursorVal.getMajorInduct (v : RecursorVal) : Name :=
-  go v.getMajorIdx v.type
-where
-  go
-  | 0, e => e.bindingDomain!.getAppFn.constName!
-  | n+1, e => go n e.bindingBody!
+def RecursorVal.getInduct (v : RecursorVal) : Name :=
+  v.name.getPrefix
 
 inductive QuotKind where
   | type  -- `Quot`

src/Lean/Elab/BuiltinCommand.lean

@@ -12,18 +12,16 @@ import Lean.Elab.Eval
 import Lean.Elab.Command
 import Lean.Elab.Open
 import Lean.Elab.SetOption
-import Init.System.Platform
 
 namespace Lean.Elab.Command
 
 @[builtin_command_elab moduleDoc] def elabModuleDoc : CommandElab := fun stx => do
-  match stx[1] with
-  | Syntax.atom _ val =>
-    let doc := val.extract 0 (val.endPos - ⟨2⟩)
-    let some range ← Elab.getDeclarationRange? stx
-      | return  -- must be from partial syntax, ignore
-    modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
-  | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
+   match stx[1] with
+   | Syntax.atom _ val =>
+     let doc := val.extract 0 (val.endPos - ⟨2⟩)
+     let range ← Elab.getDeclarationRange stx
+     modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
+   | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
 
 private def addScope (isNewNamespace : Bool) (isNoncomputable : Bool) (header : String) (newNamespace : Name) : CommandElabM Unit := do
   modify fun s => { s with
@@ -405,16 +403,6 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
       includedVars := sc.includedVars.filter (!omittedVars.contains ·) }
   | _ => throwUnsupportedSyntax
 
-@[builtin_command_elab version] def elabVersion : CommandElab := fun _ => do
-  let mut target := System.Platform.target
-  if target.isEmpty then target := "unknown"
-  -- Only one should be set, but good to know if multiple are set in error.
-  let platforms :=
-    (if System.Platform.isWindows then [" Windows"] else [])
-    ++ (if System.Platform.isOSX then [" macOS"] else [])
-    ++ (if System.Platform.isEmscripten then [" Emscripten"] else [])
-  logInfo m!"Lean {Lean.versionString}\nTarget: {target}{String.join platforms}"
-
 @[builtin_command_elab Parser.Command.exit] def elabExit : CommandElab := fun _ =>
   logWarning "using 'exit' to interrupt Lean"
 

src/Lean/Elab/BuiltinEvalCommand.lean

@@ -84,7 +84,7 @@ private def addAndCompileExprForEval (declName : Name) (value : Expr) (allowSorr
   -- An alternative design would be to make `elabTermForEval` into a term elaborator and elaborate the command all at once
   -- with `unsafe def _eval := term_for_eval% $t`, which we did try, but unwanted error messages
   -- such as "failed to infer definition type" can surface.
-  let defView := mkDefViewOfDef { isUnsafe := true, stx := ⟨.missing⟩ }
+  let defView := mkDefViewOfDef { isUnsafe := true }
     (← `(Parser.Command.definition|
           def $(mkIdent <| `_root_ ++ declName) := $(← Term.exprToSyntax value)))
   Term.elabMutualDef #[] { header := "" } #[defView]

src/Lean/Elab/DeclModifiers.lean

@@ -57,7 +57,6 @@ inductive RecKind where
 
 /-- Flags and data added to declarations (eg docstrings, attributes, `private`, `unsafe`, `partial`, ...). -/
 structure Modifiers where
-  stx             : TSyntax ``Parser.Command.declModifiers
   docString?      : Option String := none
   visibility      : Visibility := Visibility.regular
   isNoncomputable : Bool := false
@@ -122,16 +121,16 @@ section Methods
 variable [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m]
 
 /-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `protected`, `unsafe`, `noncomputable`, doc string)-/
-def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers := do
-  let docCommentStx := stx.raw[0]
-  let attrsStx      := stx.raw[1]
-  let visibilityStx := stx.raw[2]
-  let noncompStx    := stx.raw[3]
-  let unsafeStx     := stx.raw[4]
+def elabModifiers (stx : Syntax) : m Modifiers := do
+  let docCommentStx := stx[0]
+  let attrsStx      := stx[1]
+  let visibilityStx := stx[2]
+  let noncompStx    := stx[3]
+  let unsafeStx     := stx[4]
   let recKind       :=
-    if stx.raw[5].isNone then
+    if stx[5].isNone then
       RecKind.default
-    else if stx.raw[5][0].getKind == ``Parser.Command.partial then
+    else if stx[5][0].getKind == ``Parser.Command.partial then
       RecKind.partial
     else
       RecKind.nonrec
@@ -149,7 +148,7 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers :
     | none       => pure #[]
     | some attrs => elabDeclAttrs attrs
   return {
-    stx, docString?, visibility, recKind, attrs,
+    docString?, visibility, recKind, attrs,
     isUnsafe        := !unsafeStx.isNone
     isNoncomputable := !noncompStx.isNone
   }

src/Lean/Elab/Declaration.lean

@@ -104,7 +104,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   let (binders, typeStx) := expandDeclSig stx[2]
   let scopeLevelNames ← getLevelNames
   let ⟨_, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers
-  addDeclarationRanges declName modifiers.stx stx
+  addDeclarationRanges declName stx
   runTermElabM fun vars =>
     Term.withDeclName declName <| Term.withLevelNames allUserLevelNames <| Term.elabBinders binders.getArgs fun xs => do
       Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration
@@ -144,10 +144,10 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
   let (binders, type?) := expandOptDeclSig decl[2]
   let declId           := decl[1]
   let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers
-  addDeclarationRanges declName modifiers.stx decl
+  addDeclarationRanges declName decl
   let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
     -- def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
-    let mut ctorModifiers ← elabModifiers ⟨ctor[2]⟩
+    let mut ctorModifiers ← elabModifiers ctor[2]
     if let some leadingDocComment := ctor[0].getOptional? then
       if ctorModifiers.docString?.isSome then
         logErrorAt leadingDocComment "duplicate doc string"
@@ -214,18 +214,17 @@ def elabDeclaration : CommandElab := fun stx => do
     -- only case implementing incrementality currently
     elabMutualDef #[stx]
   else withoutCommandIncrementality true do
-    let modifiers : TSyntax ``Parser.Command.declModifiers := ⟨stx[0]⟩
     if declKind == ``Lean.Parser.Command.«axiom» then
-      let modifiers ← elabModifiers modifiers
+      let modifiers ← elabModifiers stx[0]
       elabAxiom modifiers decl
     else if declKind == ``Lean.Parser.Command.«inductive» then
-      let modifiers ← elabModifiers modifiers
+      let modifiers ← elabModifiers stx[0]
       elabInductive modifiers decl
     else if declKind == ``Lean.Parser.Command.classInductive then
-      let modifiers ← elabModifiers modifiers
+      let modifiers ← elabModifiers stx[0]
       elabClassInductive modifiers decl
     else if declKind == ``Lean.Parser.Command.«structure» then
-      let modifiers ← elabModifiers modifiers
+      let modifiers ← elabModifiers stx[0]
       elabStructure modifiers decl
     else
       throwError "unexpected declaration"
@@ -239,7 +238,7 @@ private def isMutualInductive (stx : Syntax) : Bool :=
 
 private def elabMutualInductive (elems : Array Syntax) : CommandElabM Unit := do
   let views ← elems.mapM fun stx => do
-     let modifiers ← elabModifiers ⟨stx[0]⟩
+     let modifiers ← elabModifiers stx[0]
      inductiveSyntaxToView modifiers stx[1]
   elabInductiveViews views
 
@@ -400,7 +399,7 @@ def elabMutual : CommandElab := fun stx => do
       -- We need to add `id`'s ranges *before* elaborating `initFn` (and then `id` itself) as
       -- otherwise the info context created by `with_decl_name` will be incomplete and break the
       -- call hierarchy
-      addDeclarationRanges fullId ⟨defStx.raw[0]⟩ defStx.raw[1]
+      addDeclarationRanges fullId defStx
       elabCommand (← `(
         $[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq
         $defStx:command))

src/Lean/Elab/DeclarationRange.lean

@@ -11,14 +11,12 @@ import Lean.Data.Lsp.Utf16
 
 namespace Lean.Elab
 
-def getDeclarationRange? [Monad m] [MonadFileMap m] (stx : Syntax) : m (Option DeclarationRange) := do
-  let some range := stx.getRange?
-    | return none
+def getDeclarationRange [Monad m] [MonadFileMap m] (stx : Syntax) : m DeclarationRange := do
   let fileMap ← getFileMap
-  --let range := fileMap.utf8RangeToLspRange
-  let pos    := fileMap.toPosition range.start
-  let endPos := fileMap.toPosition range.stop
-  return some {
+  let pos    := stx.getPos?.getD 0
+  let endPos := stx.getTailPos?.getD pos |> fileMap.toPosition
+  let pos    := pos |> fileMap.toPosition
+  return {
     pos          := pos
     charUtf16    := fileMap.leanPosToLspPos pos |>.character
     endPos       := endPos
@@ -51,27 +49,23 @@ def getDeclarationSelectionRef (stx : Syntax) : Syntax :=
 
 
 /--
-Stores the `range` and `selectionRange` for `declName` where `modsStx` is the modifier part and
-`cmdStx` the remaining part of the syntax tree for `declName`.
-
-This method is for the builtin declarations only. User-defined commands should use
-`Lean.addDeclarationRanges` to store this information for their commands.
--/
-def addDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name)
-    (modsStx : TSyntax ``Parser.Command.declModifiers) (declStx : Syntax) : m Unit := do
-  if declStx.getKind == ``Parser.Command.«example» then
+  Store the `range` and `selectionRange` for `declName` where `stx` is the whole syntax object describing `declName`.
+  This method is for the builtin declarations only.
+  User-defined commands should use `Lean.addDeclarationRanges` to store this information for their commands. -/
+def addDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (stx : Syntax) : m Unit := do
+  if stx.getKind == ``Parser.Command.«example» then
     return ()
-  let stx := mkNullNode #[modsStx, declStx]
-  -- may fail on partial syntax, ignore in that case
-  let some range ← getDeclarationRange? stx | return
-  let some selectionRange ← getDeclarationRange? (getDeclarationSelectionRef declStx) | return
-  Lean.addDeclarationRanges declName { range, selectionRange }
+  else
+    Lean.addDeclarationRanges declName {
+      range          := (← getDeclarationRange stx)
+      selectionRange := (← getDeclarationRange (getDeclarationSelectionRef stx))
+    }
 
 /-- Auxiliary method for recording ranges for auxiliary declarations (e.g., fields, nested declarations, etc. -/
 def addAuxDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (stx : Syntax) (header : Syntax) : m Unit := do
-  -- may fail on partial syntax, ignore in that case
-  let some range ← getDeclarationRange? stx | return
-  let some selectionRange ← getDeclarationRange? header | return
-  Lean.addDeclarationRanges declName { range, selectionRange }
+  Lean.addDeclarationRanges declName {
+    range          := (← getDeclarationRange stx)
+    selectionRange := (← getDeclarationRange header)
+  }
 
 end Lean.Elab

src/Lean/Elab/Frontend.lean

@@ -102,7 +102,7 @@ partial def IO.processCommandsIncrementally (inputCtx : Parser.InputContext)
 where
   go initialSnap t commands :=
     let snap := t.get
-    let commands := commands.push snap.data
+    let commands := commands.push snap.data.stx
     if let some next := snap.nextCmdSnap? then
       go initialSnap next.task commands
     else
@@ -111,15 +111,13 @@ where
       let messages := toSnapshotTree initialSnap
         |>.getAll.map (·.diagnostics.msgLog)
         |>.foldl (· ++ ·) {}
-      -- In contrast to messages, we should collect info trees only from the top-level command
-      -- snapshots as they subsume any info trees reported incrementally by their children.
-      let trees := commands.map (·.finishedSnap.get.infoTree?) |>.filterMap id |>.toPArray'
+      let trees := toSnapshotTree initialSnap
+        |>.getAll.map (·.infoTree?) |>.filterMap id |>.toPArray'
       return {
         commandState := { snap.data.finishedSnap.get.cmdState with messages, infoState.trees := trees }
         parserState := snap.data.parserState
         cmdPos := snap.data.parserState.pos
-        commands := commands.map (·.stx)
-        inputCtx, initialSnap
+        inputCtx, initialSnap, commands
       }
 
 def IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)

src/Lean/Elab/MutualDef.lean

@@ -887,7 +887,6 @@ def getKindForLetRecs (mainHeaders : Array DefViewElabHeader) : DefKind :=
   else DefKind.«def»
 
 def getModifiersForLetRecs (mainHeaders : Array DefViewElabHeader) : Modifiers := {
-  stx             := ⟨mkNullNode #[]⟩  -- ignore when computing declaration range
   isNoncomputable := mainHeaders.any fun h => h.modifiers.isNoncomputable
   recKind         := if mainHeaders.any fun h => h.modifiers.isPartial then RecKind.partial else RecKind.default
   isUnsafe        := mainHeaders.any fun h => h.modifiers.isUnsafe
@@ -998,7 +997,7 @@ where
       for view in views, header in headers do
         -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting
         -- that depends only on a part of the ref
-        addDeclarationRanges header.declName view.modifiers.stx view.ref
+        addDeclarationRanges header.declName view.ref
 
 
   processDeriving (headers : Array DefViewElabHeader) := do
@@ -1022,7 +1021,7 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
     let mut reusedAllHeaders := true
     for h : i in [0:ds.size], headerPromise in headerPromises do
       let d := ds[i]
-      let modifiers ← elabModifiers ⟨d[0]⟩
+      let modifiers ← elabModifiers d[0]
       if ds.size > 1 && modifiers.isNonrec then
         throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
       let mut view ← mkDefView modifiers d[1]

src/Lean/Elab/PreDefinition/Basic.lean

@@ -221,7 +221,7 @@ def addAndCompilePartialRec (preDefs : Array PreDefinition) : TermElabM Unit :=
               else
                 none
             | _ => none
-          modifiers := default }
+          modifiers := {} }
 
 private def containsRecFn (recFnNames : Array Name) (e : Expr) : Bool :=
   (e.find? fun e => e.isConst && recFnNames.contains e.constName!).isSome

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

@@ -212,21 +212,21 @@ def mkBRecOnMotive (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do
 /--
 Calculates the `.brecOn` functional argument corresponding to one structural recursive function.
 The `value` is the function with (only) the fixed parameters moved into the context,
-The `FType` is the expected type of the argument.
+The `type` is the expected type of the argument.
 The `recArgInfos` is used to transform the body of the function to replace recursive calls with
 uses of the `below` induction hypothesis.
 -/
 def mkBRecOnF (recArgInfos : Array RecArgInfo) (positions : Positions)
     (recArgInfo : RecArgInfo) (value : Expr) (FType : Expr) : M Expr := do
   lambdaTelescope value fun xs value => do
-    let (indicesMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
-    let FType ← instantiateForall FType indicesMajorArgs
+    let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
+    let FType ← instantiateForall FType indexMajorArgs
     forallBoundedTelescope FType (some 1) fun below _ => do
       -- TODO: `below` user name is `f`, and it will make a global `f` to be pretty printed as `_root_.f` in error messages.
       -- We should add an option to `forallBoundedTelescope` to ensure fresh names are used.
       let below := below[0]!
-      let valueNew ← replaceRecApps recArgInfos positions below value
-      mkLambdaFVars (indicesMajorArgs ++ #[below] ++ otherArgs) valueNew
+      let valueNew   ← replaceRecApps recArgInfos positions below value
+      mkLambdaFVars (indexMajorArgs ++ #[below] ++ otherArgs) valueNew
 
 /--
 Given the `motives`, figures out whether to use `.brecOn` or `.binductionOn`, pass
@@ -264,7 +264,7 @@ def inferBRecOnFTypes (recArgInfos : Array RecArgInfo) (positions : Positions)
     (brecOnConst : Nat → Expr) : MetaM (Array Expr) := do
   let numTypeFormers := positions.size
   let recArgInfo := recArgInfos[0]! -- pick an arbitrary one
-  let brecOn := brecOnConst recArgInfo.indIdx
+  let brecOn := brecOnConst 0
   check brecOn
   let brecOnType ← inferType brecOn
   -- Skip the indices and major argument

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

@@ -77,7 +77,7 @@ def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) :
       if !indIndices.all Expr.isFVar then
         throwError "its type {indInfo.name} is an inductive family and indices are not variables{indentExpr xType}"
       else if !indIndices.allDiff then
-        throwError "its type {indInfo.name} is an inductive family and indices are not pairwise distinct{indentExpr xType}"
+        throwError " its type {indInfo.name} is an inductive family and indices are not pairwise distinct{indentExpr xType}"
       else
         let indexMinPos := getIndexMinPos xs indIndices
         let numFixed    := if indexMinPos < numFixed then indexMinPos else numFixed

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

@@ -107,9 +107,9 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr
     check valueNew
     return #[{ preDef with value := valueNew }]
 
-  -- Groups the (indices of the) definitions by their position in indInfo.all
+  -- Sort the (indices of the) definitions by their position in indInfo.all
   let positions : Positions := .groupAndSort (·.indIdx) recArgInfos (Array.range indInfo.numTypeFormers)
-  trace[Elab.definition.structural] "assignments of type formers of {indInfo.name} to functions: {positions}"
+  trace[Elab.definition.structural] "positions: {positions}"
 
   -- Construct the common `.brecOn` arguments
   let motives ← (Array.zip recArgInfos values).mapM fun (r, v) => mkBRecOnMotive r v
@@ -117,7 +117,7 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr
   let brecOnConst ← mkBRecOnConst recArgInfos positions motives
   let FTypes ← inferBRecOnFTypes recArgInfos positions brecOnConst
   trace[Elab.definition.structural] "FTypes: {FTypes}"
-  let FArgs ← (recArgInfos.zip (values.zip FTypes)).mapM fun (r, (v, t)) =>
+  let FArgs ← (recArgInfos.zip  (values.zip FTypes)).mapM fun (r, (v, t)) =>
     mkBRecOnF recArgInfos positions r v t
   trace[Elab.definition.structural] "FArgs: {FArgs}"
   -- Assemble the individual `.brecOn` applications

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

@@ -15,7 +15,7 @@ partial def addSmartUnfoldingDefAux (preDef : PreDefinition) (recArgPos : Nat) :
   return { preDef with
     declName  := mkSmartUnfoldingNameFor preDef.declName
     value     := (← visit preDef.value)
-    modifiers := default
+    modifiers := {}
   }
 where
   /--

src/Lean/Elab/Structure.lean

@@ -95,7 +95,7 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
     let declName := structDeclName ++ defaultCtorName
     let ref := structStx[1].mkSynthetic
     addAuxDeclarationRanges declName ref ref
-    pure { ref, modifiers := default, name := defaultCtorName, declName }
+    pure { ref, modifiers := {}, name := defaultCtorName, declName }
   if structStx[5].isNone then
     useDefault
   else
@@ -912,7 +912,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
       let scopeLevelNames ← Term.getLevelNames
       let ⟨name, declName, allUserLevelNames⟩ ← Elab.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers
       Term.withAutoBoundImplicitForbiddenPred (fun n => name == n) do
-        addDeclarationRanges declName modifiers.stx stx
+        addDeclarationRanges declName stx
         Term.withDeclName declName do
           let ctor ← expandCtor stx modifiers declName
           let fields ← expandFields stx modifiers declName

src/Lean/Elab/Syntax.lean

@@ -146,7 +146,7 @@ where
       let args ← args.mapM fun arg => withNestedParser do process arg
       mkParserSeq args
     else
-      let args ← args.mapIdxM fun i arg => withReader (fun ctx => { ctx with first := ctx.first && i == 0 }) do process arg
+      let args ← args.mapIdxM fun i arg => withReader (fun ctx => { ctx with first := ctx.first && i.val == 0 }) do process arg
       mkParserSeq args
 
   ensureNoPrec (stx : Syntax) :=

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

@@ -65,218 +65,202 @@ def getNatOrBvValue? (ty : Expr) (expr : Expr) : M (Option Nat) := do
   | _ => return none
 
 /--
-Construct an uninterpreted `BitVec` atom from `x`.
--/
-def bitVecAtom (x : Expr) : M (Option ReifiedBVExpr) := do
-  let t ← instantiateMVars (← whnfR (← inferType x))
-  let_expr BitVec widthExpr := t | return none
-  let some width ← getNatValue? widthExpr | return none
-  let atom ← mkAtom x width
-  return some atom
-
-/--
-Reify an `Expr` that's a constant-width `BitVec`.
-Unless this function is called on something that is not a constant-width `BitVec` it is always
-going to return `some`.
+Reify an `Expr` that's a `BitVec`.
 -/
 partial def of (x : Expr) : M (Option ReifiedBVExpr) := do
-  goOrAtom x
-where
-  /--
-  Reify `x`, returns `none` if the reification procedure failed.
-  -/
-  go (x : Expr) : M (Option ReifiedBVExpr) := do
-    match_expr x with
-    | BitVec.ofNat _ _ => goBvLit x
-    | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr
-    | HOr.hOr _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.BitVec.or_congr
-    | HXor.hXor _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr
-    | HAdd.hAdd _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr
-    | HMul.hMul _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr
-    | HDiv.hDiv _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr
-    | HMod.hMod _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr
-    | Complement.complement _ _ innerExpr =>
-      unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
-    | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>
-      let distance? ← getNatOrBvValue? β distanceExpr
-      if distance?.isSome then
-        shiftConstReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftLeftConst
-          ``BVUnOp.shiftLeftConst
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeftNat_congr
-      else
-        shiftReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftLeft
-          ``BVExpr.shiftLeft
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr
-    | HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr =>
-      let distance? ← getNatOrBvValue? β distanceExpr
-      if distance?.isSome then
-        shiftConstReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftRightConst
-          ``BVUnOp.shiftRightConst
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRightNat_congr
-      else
-        shiftReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftRight
-          ``BVExpr.shiftRight
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr
-    | BitVec.sshiftRight _ innerExpr distanceExpr =>
-      let some distance ← getNatValue? distanceExpr | return none
-      shiftConstLikeReflection
-        distance
+  match_expr x with
+  | BitVec.ofNat _ _ => goBvLit x
+  | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr
+  | HOr.hOr _ _ _ _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.BitVec.or_congr
+  | HXor.hXor _ _ _ _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr
+  | HAdd.hAdd _ _ _ _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr
+  | HMul.hMul _ _ _ _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr
+  | HDiv.hDiv _ _ _ _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr
+  | HMod.hMod _ _ _ _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr
+  | Complement.complement _ _ innerExpr =>
+    unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
+  | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>
+    let distance? ← getNatOrBvValue? β distanceExpr
+    if distance?.isSome then
+      shiftConstReflection
+        β
+        distanceExpr
         innerExpr
-        .arithShiftRightConst
-        ``BVUnOp.arithShiftRightConst
-        ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr
-    | BitVec.zeroExtend _ newWidthExpr innerExpr =>
-      let some newWidth ← getNatValue? newWidthExpr | return none
-      let some inner ← goOrAtom innerExpr | return none
-      let bvExpr := .zeroExtend newWidth inner.bvExpr
-      let expr :=
-        mkApp3
-          (mkConst ``BVExpr.zeroExtend)
-          (toExpr inner.width)
-          newWidthExpr
-          inner.expr
-      let proof := do
-        let innerEval ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.zeroExtend_congr)
-          newWidthExpr
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨newWidth, bvExpr, proof, expr⟩
-    | BitVec.signExtend _ newWidthExpr innerExpr =>
-      let some newWidth ← getNatValue? newWidthExpr | return none
-      let some inner ← goOrAtom innerExpr | return none
-      let bvExpr := .signExtend newWidth inner.bvExpr
-      let expr :=
-        mkApp3
-          (mkConst ``BVExpr.signExtend)
-          (toExpr inner.width)
-          newWidthExpr
-          inner.expr
-      let proof := do
-        let innerEval ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr)
-          newWidthExpr
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨newWidth, bvExpr, proof, expr⟩
-    | 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 proof := do
-        let lhsEval ← mkEvalExpr lhs.width lhs.expr
-        let lhsProof ← lhs.evalsAtAtoms
-        let rhsProof ← rhs.evalsAtAtoms
-        let rhsEval ← mkEvalExpr rhs.width rhs.expr
-        return mkApp8 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.append_congr)
-          (toExpr lhs.width) (toExpr rhs.width)
-          lhsExpr lhsEval
-          rhsExpr rhsEval
-          lhsProof rhsProof
-      return some ⟨lhs.width + rhs.width, bvExpr, proof, expr⟩
-    | 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)
+        .shiftLeftConst
+        ``BVUnOp.shiftLeftConst
+        ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeftNat_congr
+    else
+      shiftReflection
+        β
+        distanceExpr
+        innerExpr
+        .shiftLeft
+        ``BVExpr.shiftLeft
+        ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr
+  | HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr =>
+    let distance? ← getNatOrBvValue? β distanceExpr
+    if distance?.isSome then
+      shiftConstReflection
+        β
+        distanceExpr
+        innerExpr
+        .shiftRightConst
+        ``BVUnOp.shiftRightConst
+        ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRightNat_congr
+    else
+      shiftReflection
+        β
+        distanceExpr
+        innerExpr
+        .shiftRight
+        ``BVExpr.shiftRight
+        ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr
+  | BitVec.sshiftRight _ innerExpr distanceExpr =>
+    let some distance ← getNatValue? distanceExpr | return ← ofAtom x
+    shiftConstLikeReflection
+      distance
+      innerExpr
+      .arithShiftRightConst
+      ``BVUnOp.arithShiftRightConst
+      ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr
+  | BitVec.zeroExtend _ newWidthExpr innerExpr =>
+    let some newWidth ← getNatValue? newWidthExpr | return ← ofAtom x
+    let some inner ← ofOrAtom innerExpr | return none
+    let bvExpr := .zeroExtend newWidth inner.bvExpr
+    let expr :=
+      mkApp3
+        (mkConst ``BVExpr.zeroExtend)
         (toExpr inner.width)
-        (toExpr n)
+        newWidthExpr
         inner.expr
-      let proof := do
-        let innerEval ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr)
-          (toExpr n)
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨inner.width * n, bvExpr, proof, expr⟩
-    | BitVec.extractLsb' _ startExpr lenExpr innerExpr =>
-      let some start ← getNatValue? startExpr | return none
-      let some len ← getNatValue? lenExpr | return none
-      let some inner ← goOrAtom innerExpr | return none
-      let bvExpr := .extract start len inner.bvExpr
-      let expr := mkApp4 (mkConst ``BVExpr.extract)
+    let proof := do
+      let innerEval ← mkEvalExpr inner.width inner.expr
+      let innerProof ← inner.evalsAtAtoms
+      return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.zeroExtend_congr)
+        newWidthExpr
         (toExpr inner.width)
+        innerExpr
+        innerEval
+        innerProof
+    return some ⟨newWidth, bvExpr, proof, expr⟩
+  | BitVec.signExtend _ newWidthExpr innerExpr =>
+    let some newWidth ← getNatValue? newWidthExpr | return ← ofAtom x
+    let some inner ← ofOrAtom innerExpr | return none
+    let bvExpr := .signExtend newWidth inner.bvExpr
+    let expr :=
+      mkApp3
+        (mkConst ``BVExpr.signExtend)
+        (toExpr inner.width)
+        newWidthExpr
+        inner.expr
+    let proof := do
+      let innerEval ← mkEvalExpr inner.width inner.expr
+      let innerProof ← inner.evalsAtAtoms
+      return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr)
+        newWidthExpr
+        (toExpr inner.width)
+        innerExpr
+        innerEval
+        innerProof
+    return some ⟨newWidth, bvExpr, proof, expr⟩
+  | HAppend.hAppend _ _ _ _ lhsExpr rhsExpr =>
+    let some lhs ← ofOrAtom lhsExpr | return none
+    let some rhs ← ofOrAtom 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 proof := do
+      let lhsEval ← mkEvalExpr lhs.width lhs.expr
+      let lhsProof ← lhs.evalsAtAtoms
+      let rhsProof ← rhs.evalsAtAtoms
+      let rhsEval ← mkEvalExpr rhs.width rhs.expr
+      return mkApp8 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.append_congr)
+        (toExpr lhs.width) (toExpr rhs.width)
+        lhsExpr lhsEval
+        rhsExpr rhsEval
+        lhsProof rhsProof
+    return some ⟨lhs.width + rhs.width, bvExpr, proof, expr⟩
+  | BitVec.replicate _ nExpr innerExpr =>
+    let some inner ← ofOrAtom innerExpr | return none
+    let some n ← getNatValue? nExpr | return ← ofAtom x
+    let bvExpr := .replicate n inner.bvExpr
+    let expr := mkApp3 (mkConst ``BVExpr.replicate)
+      (toExpr inner.width)
+      (toExpr n)
+      inner.expr
+    let proof := do
+      let innerEval ← mkEvalExpr inner.width inner.expr
+      let innerProof ← inner.evalsAtAtoms
+      return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr)
+        (toExpr n)
+        (toExpr inner.width)
+        innerExpr
+        innerEval
+        innerProof
+    return some ⟨inner.width * n, bvExpr, proof, expr⟩
+  | BitVec.extractLsb' _ startExpr lenExpr innerExpr =>
+    let some start ← getNatValue? startExpr | return ← ofAtom x
+    let some len ← getNatValue? lenExpr | return ← ofAtom x
+    let some inner ← ofOrAtom innerExpr | return none
+    let bvExpr := .extract start len inner.bvExpr
+    let expr := mkApp4 (mkConst ``BVExpr.extract)
+      (toExpr inner.width)
+      startExpr
+      lenExpr
+      inner.expr
+    let proof := do
+      let innerEval ← mkEvalExpr inner.width inner.expr
+      let innerProof ← inner.evalsAtAtoms
+      return mkApp6 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.extract_congr)
         startExpr
         lenExpr
-        inner.expr
-      let proof := do
-        let innerEval ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        return mkApp6 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.extract_congr)
-          startExpr
-          lenExpr
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨len, bvExpr, proof, expr⟩
-    | BitVec.rotateLeft _ innerExpr distanceExpr =>
-      rotateReflection
-        distanceExpr
+        (toExpr inner.width)
         innerExpr
-        .rotateLeft
-        ``BVUnOp.rotateLeft
-        ``Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr
-    | BitVec.rotateRight _ innerExpr distanceExpr =>
-      rotateReflection
-        distanceExpr
-        innerExpr
-        .rotateRight
-        ``BVUnOp.rotateRight
-        ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
-    | _ => return none
+        innerEval
+        innerProof
+    return some ⟨len, bvExpr, proof, expr⟩
+  | BitVec.rotateLeft _ innerExpr distanceExpr =>
+    rotateReflection
+      distanceExpr
+      innerExpr
+      .rotateLeft
+      ``BVUnOp.rotateLeft
+      ``Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr
+  | BitVec.rotateRight _ innerExpr distanceExpr =>
+    rotateReflection
+      distanceExpr
+      innerExpr
+      .rotateRight
+      ``BVUnOp.rotateRight
+      ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
+  | _ => ofAtom x
+where
+  ofAtom (x : Expr) : M (Option ReifiedBVExpr) := do
+    let t ← instantiateMVars (← whnfR (← inferType x))
+    let_expr BitVec widthExpr := t | return none
+    let some width ← getNatValue? widthExpr | return none
+    let atom ← mkAtom x width
+    return some atom
 
-  /--
-  Reify `x` or abstract it as an atom.
-  Unless this function is called on something that is not a fixed-width `BitVec` it is always going
-  to return `some`.
-  -/
-  goOrAtom (x : Expr) : M (Option ReifiedBVExpr) := do
-    let res ← go x
+  ofOrAtom (x : Expr) : M (Option ReifiedBVExpr) := do
+    let res ← of x
     match res with
     | some exp => return some exp
-    | none => bitVecAtom x
+    | none => ofAtom x
 
   shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
       (shiftOpName : Name) (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    let some inner ← goOrAtom innerExpr | return none
+    let some inner ← ofOrAtom innerExpr | return none
     let bvExpr : BVExpr inner.width := .un (shiftOp distance) inner.bvExpr
     let expr :=
       mkApp3
@@ -294,22 +278,24 @@ where
   rotateReflection (distanceExpr : Expr) (innerExpr : Expr) (rotateOp : Nat → BVUnOp)
       (rotateOpName : Name) (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    let some distance ← getNatValue? distanceExpr | return none
+    -- Either the shift values are constant or we abstract the entire term as atoms
+    let some distance ← getNatValue? distanceExpr | return ← ofAtom x
     shiftConstLikeReflection distance innerExpr rotateOp rotateOpName congrThm
 
   shiftConstReflection (β : Expr) (distanceExpr : Expr) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
       (shiftOpName : Name) (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    let some distance ← getNatOrBvValue? β distanceExpr | return none
+    -- Either the shift values are constant or we abstract the entire term as atoms
+    let some distance ← getNatOrBvValue? β distanceExpr | return ← ofAtom x
     shiftConstLikeReflection distance innerExpr shiftOp shiftOpName congrThm
 
   shiftReflection (β : Expr) (distanceExpr : Expr) (innerExpr : Expr)
       (shiftOp : {m n : Nat} → BVExpr m → BVExpr n → BVExpr m) (shiftOpName : Name)
       (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    let_expr BitVec _ ← β | return none
-    let some inner ← goOrAtom innerExpr | return none
-    let some distance ← goOrAtom distanceExpr | return none
+    let_expr BitVec _ ← β | return ← ofAtom x
+    let some inner ← of innerExpr | return none
+    let some distance ← of distanceExpr | return none
     let bvExpr : BVExpr inner.width := shiftOp inner.bvExpr distance.bvExpr
     let expr :=
       mkApp4
@@ -328,8 +314,8 @@ where
 
   binaryReflection (lhsExpr rhsExpr : Expr) (op : BVBinOp) (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    let some lhs ← goOrAtom lhsExpr | return none
-    let some rhs ← goOrAtom rhsExpr | return none
+    let some lhs ← ofOrAtom lhsExpr | return none
+    let some rhs ← ofOrAtom rhsExpr | return none
     if h : rhs.width = lhs.width then
       let bvExpr : BVExpr lhs.width := .bin lhs.bvExpr op (h ▸ rhs.bvExpr)
       let expr := mkApp4 (mkConst ``BVExpr.bin) (toExpr lhs.width) lhs.expr (toExpr op) rhs.expr
@@ -349,7 +335,7 @@ where
 
   unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    let some inner ← goOrAtom innerExpr | return none
+    let some inner ← ofOrAtom innerExpr | return none
     let bvExpr := .un op inner.bvExpr
     let expr := mkApp3 (mkConst ``BVExpr.un) (toExpr inner.width) (toExpr op) inner.expr
     let proof := unaryCongrProof inner innerExpr (mkConst congrThm)
@@ -361,7 +347,7 @@ where
     return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof
 
   goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do
-    let some ⟨width, bvVal⟩ ← getBitVecValue? x | return ← bitVecAtom x
+    let some ⟨width, bvVal⟩ ← getBitVecValue? x | return ← ofAtom x
     let bvExpr : BVExpr width := .const bvVal
     let expr := mkApp2 (mkConst ``BVExpr.const) (toExpr width) (toExpr bvVal)
     let proof := do

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

@@ -44,75 +44,40 @@ def mkTrans (x y z : Expr) (hxy hyz : Expr) : Expr :=
 def mkEvalExpr (expr : Expr) : M Expr := do
   return mkApp2 (mkConst ``BVLogicalExpr.eval) (← M.atomsAssignment) expr
 
-/--
-Construct a `ReifiedBVLogical` from `ReifiedBVPred` by wrapping it as an atom.
--/
-def ofPred  (bvPred : ReifiedBVPred) : M (Option ReifiedBVLogical) := do
-  let boolExpr := .literal bvPred.bvPred
-  let expr := mkApp2 (mkConst ``BoolExpr.literal) (mkConst ``BVPred) bvPred.expr
-  let proof := bvPred.evalsAtAtoms
-  return some ⟨boolExpr, proof, expr⟩
-
-/--
-Construct an uninterrpeted `Bool` atom from `t`.
--/
-def boolAtom (t : Expr) : M (Option ReifiedBVLogical) := do
-  let some pred ← ReifiedBVPred.boolAtom t | return none
-  ofPred pred
-
-/--
-Reify an `Expr` that is a boolean expression containing predicates about `BitVec` as atoms.
-Unless this function is called on something that is not a `Bool` it is always going to return `some`.
--/
 partial def of (t : Expr) : M (Option ReifiedBVLogical) := do
-  goOrAtom t
+  match_expr t with
+  | Bool.true =>
+    let boolExpr := .const true
+    let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.true)
+    let proof := return mkRefl (mkConst ``Bool.true)
+    return some ⟨boolExpr, proof, expr⟩
+  | Bool.false =>
+    let boolExpr := .const false
+    let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.false)
+    let proof := return mkRefl (mkConst ``Bool.false)
+    return some ⟨boolExpr, proof, expr⟩
+  | Bool.not subExpr =>
+    let some sub ← of subExpr | return none
+    let boolExpr := .not sub.bvExpr
+    let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr
+    let proof := do
+      let subEvalExpr ← mkEvalExpr sub.expr
+      let subProof ← sub.evalsAtAtoms
+      return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
+    return some ⟨boolExpr, proof, expr⟩
+  | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
+  | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
+  | BEq.beq α _ lhsExpr rhsExpr =>
+    match_expr α with
+    | Bool => gateReflection lhsExpr rhsExpr .beq ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr
+    | BitVec _ => goPred t
+    | _ => return none
+  | _ => goPred t
 where
-  /--
-  Reify `t`, returns `none` if the reification procedure failed.
-  -/
-  go (t : Expr) : M (Option ReifiedBVLogical) := do
-    match_expr t with
-    | Bool.true =>
-      let boolExpr := .const true
-      let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.true)
-      let proof := pure <| mkRefl (mkConst ``Bool.true)
-      return some ⟨boolExpr, proof, expr⟩
-    | Bool.false =>
-      let boolExpr := .const false
-      let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.false)
-      let proof := pure <| mkRefl (mkConst ``Bool.false)
-      return some ⟨boolExpr, proof, expr⟩
-    | Bool.not subExpr =>
-      let some sub ← goOrAtom subExpr | return none
-      let boolExpr := .not sub.bvExpr
-      let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr
-      let proof := do
-        let subEvalExpr ← mkEvalExpr sub.expr
-        let subProof ← sub.evalsAtAtoms
-        return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
-      return some ⟨boolExpr, proof, expr⟩
-    | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
-    | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
-    | BEq.beq α _ lhsExpr rhsExpr =>
-      match_expr α with
-      | Bool => gateReflection lhsExpr rhsExpr .beq ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr
-      | BitVec _ => goPred t
-      | _ => return none
-    | _ => goPred t
-
-  /--
-  Reify `t` or abstract it as an atom.
-  Unless this function is called on something that is not a `Bool` it is always going to return `some`.
-  -/
-  goOrAtom (t : Expr) : M (Option ReifiedBVLogical) := do
-    match ← go t with
-    | some boolExpr => return some boolExpr
-    | none => boolAtom t
-
   gateReflection (lhsExpr rhsExpr : Expr) (gate : Gate) (congrThm : Name) :
       M (Option ReifiedBVLogical) := do
-    let some lhs ← goOrAtom lhsExpr | return none
-    let some rhs ← goOrAtom rhsExpr | return none
+    let some lhs ← of lhsExpr | return none
+    let some rhs ← of rhsExpr | return none
     let boolExpr := .gate  gate lhs.bvExpr rhs.bvExpr
     let expr :=
       mkApp4
@@ -134,8 +99,11 @@ where
     return some ⟨boolExpr, proof, expr⟩
 
   goPred (t : Expr) : M (Option ReifiedBVLogical) := do
-    let some pred ← ReifiedBVPred.of t | return none
-    ofPred pred
+    let some bvPred ← ReifiedBVPred.of t | return none
+    let boolExpr := .literal bvPred.bvPred
+    let expr := mkApp2 (mkConst ``BoolExpr.literal) (mkConst ``BVPred) bvPred.expr
+    let proof := bvPred.evalsAtAtoms
+    return some ⟨boolExpr, proof, expr⟩
 
 end ReifiedBVLogical
 

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

@@ -37,68 +37,54 @@ structure ReifiedBVPred where
 namespace ReifiedBVPred
 
 /--
-Construct an uninterpreted `Bool` atom from `t`.
+Reify an `Expr` that is a proof of a predicate about `BitVec`.
 -/
-def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
-  /-
-  Idea: we have t : Bool here, let's construct:
-    BitVec.ofBool t : BitVec 1
-  as an atom. Then construct the BVPred corresponding to
-    BitVec.getLsb (BitVec.ofBool t) 0 : Bool
-  We can prove that this is equivalent to `t`. This allows us to have boolean variables in BVPred.
-  -/
-  let ty ← inferType t
-  let_expr Bool := ty | return none
-  let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1
-  let bvExpr : BVPred := .getLsbD atom.bvExpr 0
-  let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0)
-  let proof := do
-    let atomEval ← ReifiedBVExpr.mkEvalExpr atom.width atom.expr
-    let atomProof ← atom.evalsAtAtoms
-    return mkApp3
-      (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr)
-      t
-      atomEval
-      atomProof
-  return some ⟨bvExpr, proof, expr⟩
-
-/--
-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 of (t : Expr) : M (Option ReifiedBVPred) := do
-  match ← go t with
-  | some pred => return some pred
-  | none => boolAtom t
+def of (t : Expr) : M (Option ReifiedBVPred) := do
+  match_expr t with
+  | BEq.beq α _ lhsExpr rhsExpr =>
+    let_expr BitVec _ := α | return none
+    binaryReflection lhsExpr rhsExpr .eq ``Std.Tactic.BVDecide.Reflect.BitVec.beq_congr
+  | BitVec.ult _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .ult ``Std.Tactic.BVDecide.Reflect.BitVec.ult_congr
+  | BitVec.getLsbD _ subExpr idxExpr =>
+    let some sub ← ReifiedBVExpr.of subExpr | return none
+    let some idx ← getNatValue? idxExpr | return none
+    let bvExpr : BVPred := .getLsbD sub.bvExpr idx
+    let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr
+    let proof := do
+      let subEval ← ReifiedBVExpr.mkEvalExpr sub.width sub.expr
+      let subProof ← sub.evalsAtAtoms
+      return mkApp5
+        (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr)
+        idxExpr
+        (toExpr sub.width)
+        subExpr
+        subEval
+        subProof
+    return some ⟨bvExpr, proof, expr⟩
+  | _ =>
+    /-
+    Idea: we have t : Bool here, let's construct:
+      BitVec.ofBool t : BitVec 1
+    as an atom. Then construct the BVPred corresponding to
+      BitVec.getLsb (BitVec.ofBool t) 0 : Bool
+    We can prove that this is equivalent to `t`. This allows us to have boolean variables in BVPred.
+    -/
+    let ty ← inferType t
+    let_expr Bool := ty | return none
+    let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1
+    let bvExpr : BVPred := .getLsbD atom.bvExpr 0
+    let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0)
+    let proof := do
+      let atomEval ← ReifiedBVExpr.mkEvalExpr atom.width atom.expr
+      let atomProof ← atom.evalsAtAtoms
+      return mkApp3
+        (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr)
+        t
+        atomEval
+        atomProof
+    return some ⟨bvExpr, proof, expr⟩
 where
-  /--
-  Reify `t`, returns `none` if the reification procedure failed.
-  -/
-  go (t : Expr) : M (Option ReifiedBVPred) := do
-    match_expr t with
-    | BEq.beq α _ lhsExpr rhsExpr =>
-      let_expr BitVec _ := α | return none
-      binaryReflection lhsExpr rhsExpr .eq ``Std.Tactic.BVDecide.Reflect.BitVec.beq_congr
-    | BitVec.ult _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .ult ``Std.Tactic.BVDecide.Reflect.BitVec.ult_congr
-    | BitVec.getLsbD _ subExpr idxExpr =>
-      let some sub ← ReifiedBVExpr.of subExpr | return none
-      let some idx ← getNatValue? idxExpr | return none
-      let bvExpr : BVPred := .getLsbD sub.bvExpr idx
-      let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr
-      let proof := do
-        let subEval ← ReifiedBVExpr.mkEvalExpr sub.width sub.expr
-        let subProof ← sub.evalsAtAtoms
-        return mkApp5
-          (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr)
-          idxExpr
-          (toExpr sub.width)
-          subExpr
-          subEval
-          subProof
-      return some ⟨bvExpr, proof, expr⟩
-    | _ => return none
-
   binaryReflection (lhsExpr rhsExpr : Expr) (pred : BVBinPred) (congrThm : Name) :
       M (Option ReifiedBVPred) := do
     let some lhs ← ReifiedBVExpr.of lhsExpr | return none

src/Lean/Elab/Tactic/Conv/Pattern.lean

@@ -119,7 +119,7 @@ private def pre (pattern : AbstractMVarsResult) (state : IO.Ref PatternMatchStat
         let ids ← ids.mapIdxM fun i id =>
           match id.getNat with
           | 0 => throwErrorAt id "positive integer expected"
-          | n+1 => pure (n, i)
+          | n+1 => pure (n, i.1)
         let ids := ids.qsort (·.1 < ·.1)
         unless @Array.allDiff _ ⟨(·.1 == ·.1)⟩ ids do
           throwError "occurrence list is not distinct"

src/Lean/Elab/Tactic/Ext.lean

@@ -123,7 +123,9 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl
           levelParams := info.levelParams
         }
         modifyEnv fun env => addProtected env extName
-        addAuxDeclarationRanges extName (← getRef) (← getRef)
+        Lean.addDeclarationRanges extName {
+          range := ← getDeclarationRange (← getRef)
+          selectionRange := ← getDeclarationRange (← getRef) }
     catch e =>
       throwError m!"\
         Failed to generate an 'ext' theorem for '{MessageData.ofConstName structName}': {e.toMessageData}"
@@ -161,7 +163,9 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
         -- Only declarations in a namespace can be protected:
         unless extIffName.isAtomic do
           modifyEnv fun env => addProtected env extIffName
-        addAuxDeclarationRanges extName (← getRef) (← getRef)
+        Lean.addDeclarationRanges extIffName {
+          range := ← getDeclarationRange (← getRef)
+          selectionRange := ← getDeclarationRange (← getRef) }
     catch e =>
       throwError m!"\
         Failed to generate an 'ext_iff' theorem from '{MessageData.ofConstName extName}': {e.toMessageData}\n\

src/Lean/Elab/Term.lean

@@ -914,9 +914,7 @@ private def applyAttributesCore
   Remark: if the declaration has syntax errors, `declName` may be `.anonymous` see issue #4309
   In this case, we skip attribute application.
   -/
-  if declName == .anonymous then
-    return
-  withDeclName declName do
+  unless declName == .anonymous do
     for attr in attrs do
       withRef attr.stx do withLogging do
       let env ← getEnv

src/Lean/Meta/IndPredBelow.lean

@@ -54,7 +54,7 @@ def mkContext (declName : Name) : MetaM Context := do
   let typeInfos ← indVal.all.toArray.mapM getConstInfoInduct
   let motiveTypes ← typeInfos.mapM motiveType
   let motives ← motiveTypes.mapIdxM fun j motive =>
-    return (← motiveName motiveTypes j, motive)
+    return (← motiveName motiveTypes j.val, motive)
   let headers ← typeInfos.mapM $ mkHeader motives indVal.numParams
   return {
     motives := motives
@@ -214,7 +214,7 @@ def mkConstructor (ctx : Context) (i : Nat) (ctor : Name) : MetaM Constructor :=
 
 def mkInductiveType
     (ctx : Context)
-    (i : Nat)
+    (i : Fin ctx.typeInfos.size)
     (indVal : InductiveVal) : MetaM InductiveType := do
   return {
     name := ctx.belowNames[i]!
@@ -340,11 +340,11 @@ where
   mkIH
       (params : Array Expr)
       (motives : Array Expr)
-      (idx : Nat)
+      (idx : Fin ctx.motives.size)
       (motive : Name × Expr) : MetaM $ Name × (Array Expr → MetaM Expr) := do
     let name :=
       if ctx.motives.size > 1
-      then mkFreshUserName <| .mkSimple s!"ih_{idx + 1}"
+      then mkFreshUserName <| .mkSimple s!"ih_{idx.val.succ}"
       else mkFreshUserName <| .mkSimple "ih"
     let ih ← instantiateForall motive.2 params
     let mkDomain (_ : Array Expr) : MetaM Expr :=
@@ -353,7 +353,7 @@ where
         let args := params ++ motives ++ ys
         let premise :=
           mkAppN
-            (mkConst ctx.belowNames[idx]! levels) args
+            (mkConst ctx.belowNames[idx.val]! levels) args
         let conclusion :=
           mkAppN motives[idx]! ys
         mkForallFVars ys (←mkArrow premise conclusion)

src/Lean/Meta/InferType.lean

@@ -441,8 +441,6 @@ This can be used to infer the expected type of the alternatives when constructin
 -/
 def arrowDomainsN (n : Nat) (type : Expr) : MetaM (Array Expr) := do
   forallBoundedTelescope type n fun xs _ => do
-    unless xs.size = n do
-      throwError "type {type} does not have {n} parameters"
     let types ← xs.mapM (inferType ·)
     for t in types do
       if t.hasAnyFVar (fun fvar => xs.contains (.fvar fvar)) then

src/Lean/Meta/Match/CaseArraySizes.lean

@@ -70,7 +70,7 @@ def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNam
       let subst  := subgoal.subst
       let mvarId := subgoal.mvarId
       let hEqSz  := (subst.get hEq).fvarId!
-      if h : i < sizes.size then
+      if h : i.val < sizes.size then
          let n := sizes.get ⟨i, h⟩
          let mvarId ← mvarId.clear subgoal.newHs[0]!
          let mvarId ← mvarId.clear (subst.get aSizeFVarId).fvarId!

src/Lean/Meta/Match/Match.lean

@@ -545,7 +545,7 @@ private def processValue (p : Problem) : MetaM (Array Problem) := do
   let subgoals ← caseValues p.mvarId x.fvarId! values (substNewEqs := true)
   subgoals.mapIdxM fun i subgoal => do
     trace[Meta.Match.match] "processValue subgoal\n{MessageData.ofGoal subgoal.mvarId}"
-    if h : i < values.size then
+    if h : i.val < values.size then
       let value := values.get ⟨i, h⟩
       -- (x = value) branch
       let subst := subgoal.subst
@@ -599,7 +599,7 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
   let sizes := collectArraySizes p
   let subgoals ← caseArraySizes p.mvarId x.fvarId! sizes
   subgoals.mapIdxM fun i subgoal => do
-    if i < sizes.size then
+    if i.val < sizes.size then
       let size     := sizes.get! i
       let subst    := subgoal.subst
       let elems    := subgoal.elems.toList

src/Lean/Meta/Tactic/FunInd.lean

@@ -643,7 +643,7 @@ def abstractIndependentMVars (mvars : Array MVarId) (index : Nat) (e : Expr) : M
       pure mvar
   trace[Meta.FunInd] "abstractIndependentMVars, reverted mvars: {mvars}"
   let decls := mvars.mapIdx fun i mvar =>
-    (.mkSimple s!"case{i+1}", (fun _ => mvar.getType))
+    (.mkSimple s!"case{i.val+1}", (fun _ => mvar.getType))
   Meta.withLocalDeclsD decls fun xs => do
       for mvar in mvars, x in xs do
         mvar.assign x
@@ -971,7 +971,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
             mkForallFVars ys (.sort levelZero)
         let motiveArities ← infos.mapM fun info => do
           lambdaTelescope (← instantiateLambda info.value xs) fun ys _ => pure ys.size
-        let motiveDecls ← motiveTypes.mapIdxM fun i motiveType => do
+        let motiveDecls ← motiveTypes.mapIdxM fun ⟨i,_⟩ motiveType => do
           let n := if infos.size = 1 then .mkSimple "motive"
                                      else .mkSimple s!"motive_{i+1}"
           pure (n, fun _ => pure motiveType)

src/Lean/Meta/WHNF.lean

@@ -95,7 +95,7 @@ private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM Expr := do
   let majorType ← inferType major
   let majorType ← instantiateMVars (← whnf majorType)
   let majorTypeI := majorType.getAppFn
-  if !majorTypeI.isConstOf recVal.getMajorInduct then
+  if !majorTypeI.isConstOf recVal.getInduct then
     return major
   else if majorType.hasExprMVar && majorType.getAppArgs[recVal.numParams:].any Expr.hasExprMVar then
     return major
@@ -197,7 +197,7 @@ private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : A
       major ← toCtorWhenK recVal major
     major := major.toCtorIfLit
     major ← cleanupNatOffsetMajor major
-    major ← toCtorWhenStructure recVal.getMajorInduct major
+    major ← toCtorWhenStructure recVal.getInduct major
     match getRecRuleFor recVal major with
     | some rule =>
       let majorArgs := major.getAppArgs

src/Lean/Parser/Command.lean

@@ -505,9 +505,6 @@ Displays all available tactic tags, with documentation.
 -/
 @[builtin_command_parser] def printTacTags   := leading_parser
   "#print " >> nonReservedSymbol "tactic " >> nonReservedSymbol "tags"
-/-- Shows the current Lean version. Prints `Lean.versionString`. -/
-@[builtin_command_parser] def version        := leading_parser
-  "#version"
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit

src/Lean/Parser/Extra.lean

@@ -189,7 +189,7 @@ open PrettyPrinter Syntax.MonadTraverser Formatter in
 @[combinator_formatter sepByIndent]
 def sepByIndent.formatter (p : Formatter) (_sep : String) (pSep : Formatter) : Formatter := do
   let stx ← getCur
-  let hasNewlineSep := stx.getArgs.mapIdx (fun i n =>
+  let hasNewlineSep := stx.getArgs.mapIdx (fun ⟨i, _⟩ n =>
     i % 2 == 1 && n.matchesNull 0 && i != stx.getArgs.size - 1) |>.any id
   visitArgs do
     for i in (List.range stx.getArgs.size).reverse do

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1215,11 +1215,32 @@ def delabDo : Delab := whenPPOption getPPNotation do
   let items ← elems.toArray.mapM (`(doSeqItem|$(·):doElem))
   `(do $items:doSeqItem*)
 
+def reifyName : Expr → DelabM Name
+  | .const ``Lean.Name.anonymous _ => return Name.anonymous
+  | mkApp2 (.const ``Lean.Name.str _) n (.lit (.strVal s)) => return (← reifyName n).mkStr s
+  | mkApp2 (.const ``Lean.Name.num _) n (.lit (.natVal i)) => return (← reifyName n).mkNum i
+  | mkApp (.const ``Lean.Name.mkStr1 _) (.lit (.strVal a)) => return Lean.Name.mkStr1 a
+  | mkApp2 (.const ``Lean.Name.mkStr2 _) (.lit (.strVal a1)) (.lit (.strVal a2)) =>
+    return Lean.Name.mkStr2 a1 a2
+  | mkApp3 (.const ``Lean.Name.mkStr3 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) =>
+    return Lean.Name.mkStr3 a1 a2 a3
+  | mkApp4 (.const ``Lean.Name.mkStr4 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) =>
+    return Lean.Name.mkStr4 a1 a2 a3 a4
+  | mkApp5 (.const ``Lean.Name.mkStr5 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) =>
+    return Lean.Name.mkStr5 a1 a2 a3 a4 a5
+  | mkApp6 (.const ``Lean.Name.mkStr6 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) (.lit (.strVal a6)) =>
+    return Lean.Name.mkStr6 a1 a2 a3 a4 a5 a6
+  | mkApp7 (.const ``Lean.Name.mkStr7 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) (.lit (.strVal a6)) (.lit (.strVal a7)) =>
+    return Lean.Name.mkStr7 a1 a2 a3 a4 a5 a6 a7
+  | mkApp8 (.const ``Lean.Name.mkStr8 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) (.lit (.strVal a6)) (.lit (.strVal a7)) (.lit (.strVal a8)) =>
+    return Lean.Name.mkStr8 a1 a2 a3 a4 a5 a6 a7 a8
+  | _ => failure
+
 @[builtin_delab app.Lean.Name.str,
   builtin_delab app.Lean.Name.mkStr1, builtin_delab app.Lean.Name.mkStr2, builtin_delab app.Lean.Name.mkStr3, builtin_delab app.Lean.Name.mkStr4,
   builtin_delab app.Lean.Name.mkStr5, builtin_delab app.Lean.Name.mkStr6, builtin_delab app.Lean.Name.mkStr7, builtin_delab app.Lean.Name.mkStr8]
 def delabNameMkStr : Delab := whenPPOption getPPNotation do
-  let some n := (← getExpr).name? | failure
+  let n ← reifyName (← getExpr)
   -- not guaranteed to be a syntactically valid name, but usually more helpful than the explicit version
   return mkNode ``Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{n}"]
 

src/Lean/Server/Completion.lean

@@ -1004,7 +1004,7 @@ private def assignSortTexts (completions : CompletionList) : CompletionList := I
   if completions.items.isEmpty then
     return completions
   let items := completions.items.mapIdx fun i item =>
-    { item with sortText? := toString i }
+    { item with sortText? := toString i.val }
   let maxDigits := items[items.size - 1]!.sortText?.get!.length
   let items := items.map fun item =>
     let sortText := item.sortText?.get!

src/Lean/Util/Recognizers.lean

@@ -106,29 +106,4 @@ def arrayLit? (e : Expr) : Option (Expr × List Expr) :=
 def prod? (e : Expr) : Option (Expr × Expr) :=
   e.app2? ``Prod
 
-/--
-Checks if an expression is a `Name` literal, and if so returns the name.
--/
-def name? : Expr → Option Name
-  | .const ``Lean.Name.anonymous _ => Name.anonymous
-  | mkApp2 (.const ``Lean.Name.str _) n (.lit (.strVal s)) => (name? n).map (·.str s)
-  | mkApp2 (.const ``Lean.Name.num _) n i =>
-    (i.rawNatLit? <|> i.nat?).bind fun i => (name? n).map (Name.num · i)
-  | mkApp (.const ``Lean.Name.mkStr1 _) (.lit (.strVal a)) => Lean.Name.mkStr1 a
-  | mkApp2 (.const ``Lean.Name.mkStr2 _) (.lit (.strVal a1)) (.lit (.strVal a2)) =>
-    Lean.Name.mkStr2 a1 a2
-  | mkApp3 (.const ``Lean.Name.mkStr3 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) =>
-    Lean.Name.mkStr3 a1 a2 a3
-  | mkApp4 (.const ``Lean.Name.mkStr4 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) =>
-    Lean.Name.mkStr4 a1 a2 a3 a4
-  | mkApp5 (.const ``Lean.Name.mkStr5 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) =>
-    Lean.Name.mkStr5 a1 a2 a3 a4 a5
-  | mkApp6 (.const ``Lean.Name.mkStr6 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) (.lit (.strVal a6)) =>
-    Lean.Name.mkStr6 a1 a2 a3 a4 a5 a6
-  | mkApp7 (.const ``Lean.Name.mkStr7 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) (.lit (.strVal a6)) (.lit (.strVal a7)) =>
-    Lean.Name.mkStr7 a1 a2 a3 a4 a5 a6 a7
-  | mkApp8 (.const ``Lean.Name.mkStr8 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) (.lit (.strVal a6)) (.lit (.strVal a7)) (.lit (.strVal a8)) =>
-    Lean.Name.mkStr8 a1 a2 a3 a4 a5 a6 a7 a8
-  | _ => none
-
 end Lean.Expr

src/Std/Sat/AIG.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.Basic
 import Std.Sat.AIG.LawfulOperator
 import Std.Sat.AIG.Lemmas

src/Std/Sat/AIG/Basic.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Data.HashMap
 import Std.Data.HashSet
 
@@ -128,7 +127,7 @@ theorem Cache.get?_property {decls : Array (Decl α)} {idx : Nat} (c : Cache α
   induction hcache generalizing decl with
   | empty => simp at hfound
   | push_id wf ih =>
-    rw [Array.getElem_push]
+    rw [Array.get_push]
     split
     · apply ih
       simp [hfound]
@@ -140,7 +139,7 @@ theorem Cache.get?_property {decls : Array (Decl α)} {idx : Nat} (c : Cache α
       assumption
   | push_cache wf ih =>
     rename_i decl'
-    rw [Array.getElem_push]
+    rw [Array.get_push]
     split
     · simp only [HashMap.getElem?_insert] at hfound
       match heq : decl == decl' with
@@ -464,7 +463,7 @@ def mkGate (aig : AIG α) (input : GateInput aig) : Entrypoint α :=
   let cache := aig.cache.noUpdate
   have invariant := by
     intro i lhs' rhs' linv' rinv' h1 h2
-    simp only [Array.getElem_push] at h2
+    simp only [Array.get_push] at h2
     split at h2
     · apply aig.invariant <;> assumption
     · injections
@@ -483,7 +482,7 @@ def mkAtom (aig : AIG α) (n : α) : Entrypoint α :=
   let cache := aig.cache.noUpdate
   have invariant := by
     intro i lhs rhs linv rinv h1 h2
-    simp only [Array.getElem_push] at h2
+    simp only [Array.get_push] at h2
     split at h2
     · apply aig.invariant <;> assumption
     · contradiction
@@ -499,7 +498,7 @@ def mkConst (aig : AIG α) (val : Bool) : Entrypoint α :=
   let cache := aig.cache.noUpdate
   have invariant := by
     intro i lhs rhs linv rinv h1 h2
-    simp only [Array.getElem_push] at h2
+    simp only [Array.get_push] at h2
     split at h2
     · apply aig.invariant <;> assumption
     · contradiction

src/Std/Sat/AIG/CNF.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.CNF
 import Std.Sat.AIG.Basic
 import Std.Sat.AIG.Lemmas

src/Std/Sat/AIG/Cached.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.Basic
 import Std.Sat.AIG.Lemmas
 
@@ -36,7 +35,7 @@ def mkAtomCached (aig : AIG α) (n : α) : Entrypoint α :=
     let decls := decls.push decl
     have inv := by
       intro i lhs rhs linv rinv h1 h2
-      simp only [Array.getElem_push] at h2
+      simp only [Array.get_push] at h2
       split at h2
       · apply inv <;> assumption
       · contradiction
@@ -58,7 +57,7 @@ def mkConstCached (aig : AIG α) (val : Bool) : Entrypoint α :=
     let decls := decls.push decl
     have inv := by
       intro i lhs rhs linv rinv h1 h2
-      simp only [Array.getElem_push] at h2
+      simp only [Array.get_push] at h2
       split at h2
       · apply inv <;> assumption
       · contradiction
@@ -121,7 +120,7 @@ where
           have inv := by
             intro i lhs rhs linv rinv h1 h2
             simp only [decls] at *
-            simp only [Array.getElem_push] at h2
+            simp only [Array.get_push] at h2
             split at h2
             · apply inv <;> assumption
             · injections; omega

src/Std/Sat/AIG/CachedGates.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.Cached
 import Std.Sat.AIG.CachedLemmas
 

src/Std/Sat/AIG/CachedGatesLemmas.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.CachedGates
 import Std.Sat.AIG.LawfulOperator
 

src/Std/Sat/AIG/CachedLemmas.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.Cached
 
 /-!
@@ -60,7 +59,7 @@ theorem mkAtomCached_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < ai
     simp [this]
   | none =>
     have := mkAtomCached_miss_aig aig hcache
-    simp only [this, Array.getElem_push]
+    simp only [this, Array.get_push]
     split
     · rfl
     · contradiction
@@ -134,7 +133,7 @@ theorem mkConstCached_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx <
     simp [this]
   | none =>
     have := mkConstCached_miss_aig aig hcache
-    simp only [this, Array.getElem_push]
+    simp only [this, Array.get_push]
     split
     · rfl
     · contradiction
@@ -257,7 +256,7 @@ theorem mkGateCached.go_decl_eq (aig : AIG α) (input : GateInput aig) :
           · rw [← hres]
             dsimp only
             intro idx h1 h2
-            rw [Array.getElem_push]
+            rw [Array.get_push]
             simp [h2]
 
 /--

src/Std/Sat/AIG/If.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.CachedGatesLemmas
 import Std.Sat.AIG.LawfulVecOperator
 

src/Std/Sat/AIG/LawfulOperator.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.Basic
 
 /-!

src/Std/Sat/AIG/LawfulVecOperator.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.LawfulOperator
 import Std.Sat.AIG.RefVec
 

src/Std/Sat/AIG/Lemmas.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.Basic
 import Std.Sat.AIG.LawfulOperator
 
@@ -78,7 +77,7 @@ The AIG produced by `AIG.mkGate` agrees with the input AIG on all indices that a
 theorem mkGate_decl_eq idx (aig : AIG α) (input : GateInput aig) {h : idx < aig.decls.size} :
     have := mkGate_le_size aig input
     (aig.mkGate input).aig.decls[idx]'(by omega) = aig.decls[idx] := by
-  simp only [mkGate, Array.getElem_push]
+  simp only [mkGate, Array.get_push]
   split
   · rfl
   · contradiction
@@ -99,13 +98,13 @@ theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
     unfold denote denote.go
   split
   · next heq =>
-    rw [mkGate, Array.getElem_push_eq] at heq
+    rw [mkGate, Array.get_push_eq] at heq
     contradiction
   · next heq =>
-    rw [mkGate, Array.getElem_push_eq] at heq
+    rw [mkGate, Array.get_push_eq] at heq
     contradiction
   · next heq =>
-    rw [mkGate, Array.getElem_push_eq] at heq
+    rw [mkGate, Array.get_push_eq] at heq
     injection heq with heq1 heq2 heq3 heq4
     dsimp only
     congr 2
@@ -132,7 +131,7 @@ The AIG produced by `AIG.mkAtom` agrees with the input AIG on all indices that a
 -/
 theorem mkAtom_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < aig.decls.size} {hbound} :
     (aig.mkAtom var).aig.decls[idx]'hbound = aig.decls[idx] := by
-  simp only [mkAtom, Array.getElem_push]
+  simp only [mkAtom, Array.get_push]
   split
   · rfl
   · contradiction
@@ -149,14 +148,14 @@ theorem denote_mkAtom {aig : AIG α} :
   unfold denote denote.go
   split
   · next heq =>
-    rw [mkAtom, Array.getElem_push_eq] at heq
+    rw [mkAtom, Array.get_push_eq] at heq
     contradiction
   · next heq =>
-    rw [mkAtom, Array.getElem_push_eq] at heq
+    rw [mkAtom, Array.get_push_eq] at heq
     injection heq with heq
     rw [heq]
   · next heq =>
-    rw [mkAtom, Array.getElem_push_eq] at heq
+    rw [mkAtom, Array.get_push_eq] at heq
     contradiction
 
 /--
@@ -172,7 +171,7 @@ The AIG produced by `AIG.mkConst` agrees with the input AIG on all indices that
 theorem mkConst_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx < aig.decls.size} :
     have := mkConst_le_size aig val
     (aig.mkConst val).aig.decls[idx]'(by omega) = aig.decls[idx] := by
-  simp only [mkConst, Array.getElem_push]
+  simp only [mkConst, Array.get_push]
   split
   · rfl
   · contradiction
@@ -188,14 +187,14 @@ theorem denote_mkConst {aig : AIG α} : ⟦(aig.mkConst val), assign⟧ = val :=
   unfold denote denote.go
   split
   · next heq =>
-    rw [mkConst, Array.getElem_push_eq] at heq
+    rw [mkConst, Array.get_push_eq] at heq
     injection heq with heq
     rw [heq]
   · next heq =>
-    rw [mkConst, Array.getElem_push_eq] at heq
+    rw [mkConst, Array.get_push_eq] at heq
     contradiction
   · next heq =>
-    rw [mkConst, Array.getElem_push_eq] at heq
+    rw [mkConst, Array.get_push_eq] at heq
     contradiction
 
 /--

src/Std/Sat/AIG/RefVec.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.LawfulOperator
 import Std.Sat.AIG.CachedGatesLemmas
 
@@ -59,7 +58,7 @@ def push (s : RefVec aig len) (ref : AIG.Ref aig) : RefVec aig (len + 1) :=
     by simp [hlen],
     by
       intro i hi
-      simp only [Array.getElem_push]
+      simp only [Array.get_push]
       split
       · apply hrefs
         omega
@@ -85,7 +84,7 @@ theorem get_push_ref_lt (s : RefVec aig len) (ref : AIG.Ref aig) (idx : Nat)
   simp only [get, push, Ref.mk.injEq]
   cases ref
   simp only [Ref.mk.injEq]
-  rw [Array.getElem_push_lt]
+  rw [Array.get_push_lt]
 
 @[simp]
 theorem get_cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (idx : Nat) (hidx : idx < len)

src/Std/Sat/AIG/RefVecOperator.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.RefVecOperator.Map
 import Std.Sat.AIG.RefVecOperator.Zip
 import Std.Sat.AIG.RefVecOperator.Fold

src/Std/Sat/AIG/RefVecOperator/Fold.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.RefVec
 import Std.Sat.AIG.LawfulVecOperator
 

src/Std/Sat/AIG/RefVecOperator/Map.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.RefVec
 import Std.Sat.AIG.LawfulVecOperator
 

src/Std/Sat/AIG/RefVecOperator/Zip.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.RefVec
 import Std.Sat.AIG.LawfulVecOperator
 

src/Std/Sat/AIG/Relabel.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.Basic
 import Std.Sat.AIG.Lemmas
 

src/Std/Sat/AIG/RelabelNat.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
 import Std.Sat.AIG.Relabel
 
 

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
-import Init.Data.AC
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Const
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Not

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -111,7 +111,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           ⟨units.size, units_size_lt_updatedUnits_size⟩
         have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1
         refine ⟨mostRecentUnitIdx, l.2, i_gt_zero, ?_⟩
-        simp only [insertUnit, h3, ite_false, Array.getElem_push_eq, i_eq_l, reduceCtorEq]
+        simp only [insertUnit, h3, ite_false, Array.get_push_eq, i_eq_l, reduceCtorEq]
         constructor
         · rfl
         · constructor
@@ -132,7 +132,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                 · intro h
                   simp only [← h, not_true, mostRecentUnitIdx] at hk
                   exact hk rfl
-              rw [Array.getElem_push_lt _ _ _ k_in_bounds]
+              rw [Array.get_push_lt _ _ _ k_in_bounds]
               rw [i_eq_l] at h2
               exact h2 ⟨k.1, k_in_bounds⟩
       · next i_ne_l =>
@@ -142,7 +142,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
         constructor
         · exact h1
         · intro j
-          rw [Array.getElem_push]
+          rw [Array.get_push]
           by_cases h : j.val < Array.size units
           · simp only [h, dite_true]
             exact h2 ⟨j.1, h⟩
@@ -189,9 +189,9 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           exact h5 (has_add _ true)
         | true, false =>
           refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, mostRecentUnitIdx, i_gt_zero, ?_⟩
-          simp only [insertUnit, h5, ite_false, Array.getElem_push_eq, ne_eq, reduceCtorEq]
+          simp only [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq, reduceCtorEq]
           constructor
-          · rw [Array.getElem_push_lt units l j.1 j.2, h1]
+          · rw [Array.get_push_lt units l j.1 j.2, h1]
           · constructor
             · simp [i_eq_l, ← hl]
               rfl
@@ -210,7 +210,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                     simp [hasAssignment, hl, getElem!, l_in_bounds, h2, hasNegAssignment, decidableGetElem?] at h5
                   | both => simp (config := {decide := true}) only [h] at h3
                 · intro k k_ne_j k_ne_l
-                  rw [Array.getElem_push]
+                  rw [Array.get_push]
                   by_cases h : k.1 < units.size
                   · simp only [h, dite_true]
                     have k_ne_j : ⟨k.1, h⟩ ≠ j := by
@@ -226,12 +226,12 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                       exact k_ne_l rfl
         | false, true =>
           refine ⟨mostRecentUnitIdx, ⟨j.1, j_lt_updatedUnits_size⟩, i_gt_zero, ?_⟩
-          simp [insertUnit, h5, ite_false, Array.getElem_push_eq, ne_eq]
+          simp [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq]
           constructor
           · simp [i_eq_l, ← hl]
             rfl
           · constructor
-            · rw [Array.getElem_push_lt units l j.1 j.2, h1]
+            · rw [Array.get_push_lt units l j.1 j.2, h1]
             · constructor
               · simp only [i_eq_l]
                 rw [Array.getElem_modify_self]
@@ -247,7 +247,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                   | neg  => simp (config := {decide := true}) only [h] at h3
                   | both => simp (config := {decide := true}) only [h] at h3
                 · intro k k_ne_l k_ne_j
-                  rw [Array.getElem_push]
+                  rw [Array.get_push]
                   by_cases h : k.1 < units.size
                   · simp only [h, dite_true]
                     have k_ne_j : ⟨k.1, h⟩ ≠ j := by
@@ -275,13 +275,13 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
         refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, b,i_gt_zero, ?_⟩
         simp only [insertUnit, h5, ite_false, reduceCtorEq]
         constructor
-        · rw [Array.getElem_push_lt units l j.1 j.2, h1]
+        · rw [Array.get_push_lt units l j.1 j.2, h1]
         · constructor
           · rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h2]
           · constructor
             · exact h3
             · intro k k_ne_j
-              rw [Array.getElem_push]
+              rw [Array.get_push]
               by_cases h : k.val < units.size
               · simp only [h, dite_true]
                 have k_ne_j : ⟨k.1, h⟩ ≠ j := by
@@ -307,11 +307,11 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
     constructor
     · split
       · exact h1
-      · simp only [Array.getElem_push_lt units l j1.1 j1.2, h1]
+      · simp only [Array.get_push_lt units l j1.1 j1.2, h1]
     · constructor
       · split
         · exact h2
-        · simp only [Array.getElem_push_lt units l j2.1 j2.2, h2]
+        · simp only [Array.get_push_lt units l j2.1 j2.2, h2]
       · constructor
         · split
           · exact h3
@@ -336,7 +336,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
               split
               · exact h5 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
               · simp only [ne_eq]
-                rw [Array.getElem_push]
+                rw [Array.get_push]
                 simp only [k_in_bounds, dite_true]
                 exact h5 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
             · next k_not_lt_units_size =>
@@ -354,7 +354,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                   rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
                   · exfalso; exact k_not_lt_units_size k_lt_units_size
                   · exact k_eq_units_size
-                simp only [k_eq_units_size, Array.getElem_push_eq, ne_eq]
+                simp only [k_eq_units_size, Array.get_push_eq, ne_eq]
                 intro l_eq_i
                 simp [getElem!, l_eq_i, i_in_bounds, h3, has_both, decidableGetElem?] at h
 

src/kernel/declaration.cpp

@@ -126,6 +126,7 @@ constructor_val::constructor_val(name const & n, names const & lparams, expr con
     object_ref(lean_mk_constructor_val(n.to_obj_arg(), lparams.to_obj_arg(), type.to_obj_arg(), induct.to_obj_arg(),
                                        nat(cidx).to_obj_arg(), nat(nparams).to_obj_arg(), nat(nfields).to_obj_arg(), is_unsafe)) {
 }
+
 bool constructor_val::is_unsafe() const { return lean_constructor_val_is_unsafe(to_obj_arg()); }
 
 extern "C" object * lean_mk_recursor_val(object * n, object * lparams, object * type, object * all,
@@ -142,18 +143,6 @@ recursor_val::recursor_val(name const & n, names const & lparams, expr const & t
                                     nat(nminors).to_obj_arg(), rules.to_obj_arg(), k, is_unsafe)) {
 }
 
-name const & recursor_val::get_major_induct() const {
-    unsigned int n = get_major_idx();
-    expr const * t = &(to_constant_val().get_type());
-    for (unsigned int i = 0; i < n; i++) {
-        t = &(binding_body(*t));
-    }
-    t = &(binding_domain(*t));
-    t = &(get_app_fn(*t));
-    return const_name(*t);
-}
-
-
 bool recursor_val::is_k() const { return lean_recursor_k(to_obj_arg()); }
 bool recursor_val::is_unsafe() const { return lean_recursor_is_unsafe(to_obj_arg()); }
 

src/kernel/declaration.h

@@ -370,7 +370,7 @@ public:
     recursor_val & operator=(recursor_val && other) { object_ref::operator=(std::move(other)); return *this; }
     constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
     name const & get_name() const { return to_constant_val().get_name(); }
-    name const & get_major_induct() const;
+    name const & get_induct() const { return get_name().get_prefix(); }
     names const & get_all() const { return static_cast<names const &>(cnstr_get_ref(*this, 1)); }
     unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
     unsigned get_nindices() const { return static_cast<nat const &>(cnstr_get_ref(*this, 3)).get_small_value(); }

src/kernel/expr.cpp

@@ -79,22 +79,21 @@ extern "C" object * lean_lit_type(obj_arg e);
 expr lit_type(literal const & lit) { return expr(lean_lit_type(lit.to_obj_arg())); }
 
 extern "C" uint64_t lean_expr_hash(obj_arg e);
-unsigned hash_core(expr const & e) {
-    return lean_expr_hash(e.to_obj_arg());
+unsigned hash(expr const & e) {
+    object * o = e.raw();
+    unsigned r = static_cast<unsigned>(lean_ctor_get_uint64(o, lean_ctor_num_objs(o)*sizeof(object*)));
+    lean_assert(r == lean_expr_hash(e.to_obj_arg()));
+    return r;
 }
 
 extern "C" uint8 lean_expr_has_fvar(obj_arg e);
-bool has_fvar_core(expr const & e) {
-    return lean_expr_has_fvar(e.to_obj_arg());
-}
+bool has_fvar(expr const & e) { return lean_expr_has_fvar(e.to_obj_arg()); }
 
 extern "C" uint8 lean_expr_has_expr_mvar(obj_arg e);
-bool has_expr_mvar_core(expr const & e) {
-    return lean_expr_has_expr_mvar(e.to_obj_arg());
-}
+bool has_expr_mvar(expr const & e) { return lean_expr_has_expr_mvar(e.to_obj_arg()); }
 
 extern "C" uint8 lean_expr_has_level_mvar(obj_arg e);
-bool has_univ_mvar_core(expr const & e) { return lean_expr_has_level_mvar(e.to_obj_arg()); }
+bool has_univ_mvar(expr const & e) { return lean_expr_has_level_mvar(e.to_obj_arg()); }
 
 extern "C" uint8 lean_expr_has_level_param(obj_arg e);
 bool has_univ_param(expr const & e) { return lean_expr_has_level_param(e.to_obj_arg()); }

src/kernel/expr.h

@@ -123,37 +123,11 @@ inline bool is_eqp(optional<expr> const & a, optional<expr> const & b) {
     return static_cast<bool>(a) == static_cast<bool>(b) && (!a || is_eqp(*a, *b));
 }
 
-inline uint64_t get_data(expr const & e) {
-    return lean_ctor_get_uint64(e.raw(), lean_ctor_num_objs(e.raw())*sizeof(object*));
-}
-/* This is the implementation in Lean */
-unsigned hash_core(expr const & e);
-inline unsigned hash(expr const & e) {
-    unsigned r = static_cast<unsigned>(get_data(e));
-    lean_assert(r == hash_core(e));
-    return r;
-}
-/* This is the implementation in Lean */
-bool has_expr_mvar_core(expr const & e);
-inline bool has_expr_mvar(expr const & e) {
-    bool r = ((get_data(e) >> 41) & 1) == 1;
-    lean_assert(r == has_expr_mvar_core(e)); // ensure the C++ implementation matches the Lean one.
-    return r;
-}
-bool has_univ_mvar_core(expr const & e);
-inline bool has_univ_mvar(expr const & e) {
-    bool r = ((get_data(e) >> 42) & 1) == 1;
-    lean_assert(r == has_univ_mvar_core(e)); // ensure the C++ implementation matches the Lean one.
-    return r;
-}
+unsigned hash(expr const & e);
+bool has_expr_mvar(expr const & e);
+bool has_univ_mvar(expr const & e);
 inline bool has_mvar(expr const & e) { return has_expr_mvar(e) || has_univ_mvar(e); }
-/* This is the implementation in Lean */
-bool has_fvar_core(expr const & e);
-inline bool has_fvar(expr const & e) {
-    bool r = ((get_data(e) >> 40) & 1) == 1;
-    lean_assert(r == has_fvar_core(e)); // ensure the C++ implementation matches the Lean one.
-    return r;
-}
+bool has_fvar(expr const & e);
 bool has_univ_param(expr const & e);
 unsigned get_loose_bvar_range(expr const & e);
 

src/kernel/inductive.h

@@ -33,7 +33,7 @@ inline expr to_cnstr_when_K(environment const & env, recursor_val const & rval,
     lean_assert(rval.is_k());
     expr app_type    = whnf(infer_type(e));
     expr const & app_type_I = get_app_fn(app_type);
-    if (!is_constant(app_type_I) || const_name(app_type_I) != rval.get_major_induct()) return e; // type incorrect
+    if (!is_constant(app_type_I) || const_name(app_type_I) != rval.get_induct()) return e; // type incorrect
     if (has_expr_mvar(app_type)) {
         buffer<expr> app_type_args;
         get_app_args(app_type, app_type_args);
@@ -94,7 +94,7 @@ inline optional<expr> inductive_reduce_rec(environment const & env, expr const &
     else if (is_string_lit(major))
         major = string_lit_to_constructor(major);
     else
-        major = to_cnstr_when_structure(env, rec_val.get_major_induct(), major, whnf, infer_type);
+        major = to_cnstr_when_structure(env, rec_val.get_induct(), major, whnf, infer_type);
     optional<recursor_rule> rule = get_rec_rule_for(rec_val, major);
     if (!rule) return none_expr();
     buffer<expr> major_args;

src/lake/Lake/Build/Executable.lean

@@ -6,7 +6,6 @@ Authors: Mac Malone
 import Lake.Build.Common
 
 namespace Lake
-open System (FilePath)
 
 /-! # Lean Executable Build
 The build function definition for a Lean executable.

src/lake/Lake/Build/Facets.lean

@@ -16,8 +16,7 @@ definitions.
 -/
 
 namespace Lake
-open Lean (Name)
-open System (SearchPath FilePath)
+export System (SearchPath FilePath)
 
 /-- A dynamic/shared library for linking. -/
 structure Dynlib where

src/lake/Lake/Build/Index.lean

@@ -17,7 +17,6 @@ This module leverages the index to perform topologically-based recursive builds.
 
 open Lean
 namespace Lake
-open System (FilePath)
 
 /--
 Converts a conveniently-typed target facet build function into its

src/lake/Lake/Build/Info.lean

@@ -16,7 +16,6 @@ the build.
 -/
 
 namespace Lake
-open Lean (Name)
 
 /-- The type of Lake's build info. -/
 inductive BuildInfo

src/lake/Lake/Build/Key.lean

@@ -6,7 +6,6 @@ Authors: Mac Malone
 import Lake.Util.Name
 
 namespace Lake
-open Lean (Name)
 
 /-- The type of keys in the Lake build store. -/
 inductive BuildKey

src/lake/Lake/Build/Library.lean

@@ -11,7 +11,6 @@ Build function definitions for a library's builtin facets.
 -/
 
 namespace Lake
-open System (FilePath)
 
 /-! ## Build Lean & Static Lib -/
 

src/lake/Lake/Build/Package.lean

@@ -15,7 +15,6 @@ Build function definitions for a package's builtin facets.
 
 open System
 namespace Lake
-open Lean (Name)
 
 /-- Compute a topological ordering of the package's transitive dependencies. -/
 def Package.recComputeDeps (self : Package) : FetchM (Array Package) := do

src/lake/Lake/Build/Store.lean

@@ -15,7 +15,6 @@ topological-based build of an initial key's dependencies).
 -/
 
 namespace Lake
-open Lean (Name NameMap)
 
 /-- A monad equipped with a Lake build store. -/
 abbrev MonadBuildStore (m) := MonadDStore BuildKey BuildData m

src/lake/Lake/Build/Targets.lean

@@ -10,8 +10,6 @@ Utilities for fetching package, library, module, and executable targets and face
 -/
 
 namespace Lake
-open Lean (Name)
-open System (FilePath)
 
 /-! ## Package Facets & Targets -/
 

src/lake/Lake/CLI/Actions.lean

@@ -8,8 +8,6 @@ import Lake.Build.Targets
 import Lake.CLI.Build
 
 namespace Lake
-open Lean (Name)
-open System (FilePath)
 
 def env (cmd : String) (args : Array String := #[]) : LakeT IO UInt32 := do
   IO.Process.spawn {cmd, args, env := ← getAugmentedEnv} >>= (·.wait)

src/lake/Lake/CLI/Build.lean

@@ -7,7 +7,6 @@ import Lake.Build.Index
 import Lake.CLI.Error
 
 namespace Lake
-open Lean (Name)
 
 /-! ## Build Target Specifiers -/
 

src/lake/Lake/CLI/Init.lean

@@ -13,7 +13,6 @@ import Lake.Build.Actions
 
 namespace Lake
 open Git System
-open Lean (Name)
 
 /-- The default module of an executable in `std` package. -/
 def defaultExeRoot : Name := `Main

src/lake/Lake/CLI/Main.lean

@@ -19,7 +19,7 @@ import Lake.CLI.Serve
 -- # CLI
 
 open System
-open Lean (Json toJson fromJson? LeanPaths NameMap)
+open Lean (Json toJson fromJson? LeanPaths)
 
 namespace Lake
 

src/lake/Lake/CLI/Serve.lean

@@ -10,7 +10,6 @@ import Lean.Util.FileSetupInfo
 
 namespace Lake
 open Lean
-open System (FilePath)
 
 /-- Exit code to return if `setup-file` cannot find the config file. -/
 def noConfigFileCode : ExitCode := 2

src/lake/Lake/Config/ExternLib.lean

@@ -6,7 +6,6 @@ Authors: Mac Malone
 import Lake.Config.Package
 
 namespace Lake
-open Lean (Name)
 
 /-- An external library -- its package plus its configuration. -/
 structure ExternLib where

src/lake/Lake/Config/FacetConfig.lean

@@ -6,7 +6,6 @@ Authors: Mac Malone, Mario Carneiro
 import Lake.Build.Fetch
 
 namespace Lake
-open Lean (Name)
 
 /-- A facet's declarative configuration. -/
 structure FacetConfig (DataFam : Name → Type) (ι : Type) (name : Name) : Type where

src/lake/Lake/Config/Monad.lean

@@ -7,7 +7,7 @@ import Lake.Config.Context
 import Lake.Config.Workspace
 
 open System
-open Lean (Name NameMap)
+open Lean (Name)
 
 /-! # Lake Configuration Monads
 Definitions and helpers for interacting with the Lake configuration monads.

src/lake/Lake/Config/TargetConfig.lean

@@ -6,7 +6,6 @@ Authors: Mac Malone
 import Lake.Build.Fetch
 
 namespace Lake
-open Lean (Name)
 
 /-- A custom target's declarative configuration. -/
 structure TargetConfig (pkgName name : Name) : Type where

src/lake/Lake/Config/Workspace.lean

@@ -12,7 +12,6 @@ import Lake.Util.Log
 open System
 
 namespace Lake
-open Lean (Name)
 
 /-- A Lake workspace -- the top-level package directory. -/
 structure Workspace : Type where

src/lake/Lake/DSL/Targets.lean

@@ -12,7 +12,6 @@ Macros for declaring Lake targets and facets.
 
 namespace Lake.DSL
 open Lean Parser Command
-open System (FilePath)
 
 syntax buildDeclSig :=
   identOrStr (ppSpace simpleBinder)? Term.typeSpec declValSimple

src/lake/Lake/Load/Package.lean

@@ -15,7 +15,6 @@ from Lake configuration file (either Lean or TOML).
 open Lean
 
 namespace Lake
-open System (FilePath)
 
 /--
 Return whether a configuration file with the given name

src/lake/Lake/Load/Toml.lean

@@ -17,7 +17,6 @@ Lake configuration file written in TOML.
 -/
 
 namespace Lake
-open System (FilePath)
 
 open Toml
 

src/lake/Lake/Util/Name.lean

@@ -11,7 +11,8 @@ import Lake.Util.RBArray
 open Lean
 
 namespace Lake
-open Lean (Name NameMap)
+
+export Lean (Name NameMap)
 
 /--
 First tries to convert a string into a legal name.