chore: fix apply? error reporting when out of heartbeats

src/Init/Data/Array/Attach.lean

@@ -10,13 +10,12 @@ import Init.Data.List.Attach
 
 namespace Array
 
-/--
-`O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on
-`a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l`
-but is defined only when all members of `l` satisfy `P`, using the proof
-to apply `f`.
+/-- `O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on
+  `a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l`
+  but is defined only when all members of `l` satisfy `P`, using the proof
+  to apply `f`.
 
-We replace this at runtime with a more efficient version via the `csimp` lemma `pmap_eq_pmapImpl`.
+We replace this at runtime with a more efficient version via
 -/
 def pmap {P : α → Prop} (f : ∀ a, P a → β) (l : Array α) (H : ∀ a ∈ l, P a) : Array β :=
   (l.toList.pmap f (fun a m => H a (mem_def.mpr m))).toArray
@@ -74,17 +73,6 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
   intro a m h₁ h₂
   congr
 
-@[simp] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
-
-@[simp] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (l : Array α) (h : ∀ b ∈ l.push a, P b) :
-    pmap f (l.push a) h =
-      (pmap f l (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp))) := by
-  simp [pmap]
-
-@[simp] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
-
-@[simp] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #[], P x) : (#[] : Array α).attachWith P H = #[] := rfl
-
 @[simp] theorem _root_.List.attachWith_mem_toArray {l : List α} :
     l.attachWith (fun x => x ∈ l.toArray) (fun x h => by simpa using h) =
       l.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
@@ -92,353 +80,6 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
   apply List.pmap_congr_left
   simp
 
-@[simp]
-theorem pmap_eq_map (p : α → Prop) (f : α → β) (l : Array α) (H) :
-    @pmap _ _ p (fun a _ => f a) l H = map f l := by
-  cases l; simp
-
-theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (l : Array α) {H₁ H₂}
-    (h : ∀ a ∈ l, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f l H₁ = pmap g l H₂ := by
-  cases l
-  simp only [mem_toArray] at h
-  simp only [List.pmap_toArray, mk.injEq]
-  rw [List.pmap_congr_left _ h]
-
-theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (l H) :
-    map g (pmap f l H) = pmap (fun a h => g (f a h)) l H := by
-  cases l
-  simp [List.map_pmap]
-
-theorem pmap_map {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β) (l H) :
-    pmap g (map f l) H = pmap (fun a h => g (f a) h) l fun _ h => H _ (mem_map_of_mem _ h) := by
-  cases l
-  simp [List.pmap_map]
-
-theorem attach_congr {l₁ l₂ : Array α} (h : l₁ = l₂) :
-    l₁.attach = l₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩) := by
-  subst h
-  simp
-
-theorem attachWith_congr {l₁ l₂ : Array α} (w : l₁ = l₂) {P : α → Prop} {H : ∀ x ∈ l₁, P x} :
-    l₁.attachWith P H = l₂.attachWith P fun _ h => H _ (w ▸ h) := by
-  subst w
-  simp
-
-@[simp] theorem attach_push {a : α} {l : Array α} :
-    (l.push a).attach =
-      (l.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by
-  cases l
-  rw [attach_congr (List.push_toArray _ _)]
-  simp [Function.comp_def]
-
-@[simp] theorem attachWith_push {a : α} {l : Array α} {P : α → Prop} {H : ∀ x ∈ l.push a, P x} :
-    (l.push a).attachWith P H =
-      (l.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩ := by
-  cases l
-  simp [attachWith_congr (List.push_toArray _ _)]
-
-theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) :
-    pmap f l H = l.attach.map fun x => f x.1 (H _ x.2) := by
-  cases l
-  simp [List.pmap_eq_map_attach]
-
-theorem attach_map_coe (l : Array α) (f : α → β) :
-    (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
-  cases l
-  simp [List.attach_map_coe]
-
-theorem attach_map_val (l : Array α) (f : α → β) : (l.attach.map fun i => f i.val) = l.map f :=
-  attach_map_coe _ _
-
-@[simp]
-theorem attach_map_subtype_val (l : Array α) : l.attach.map Subtype.val = l := by
-  cases l; simp
-
-theorem attachWith_map_coe {p : α → Prop} (f : α → β) (l : Array α) (H : ∀ a ∈ l, p a) :
-    ((l.attachWith p H).map fun (i : { i // p i}) => f i) = l.map f := by
-  cases l; simp
-
-theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : Array α) (H : ∀ a ∈ l, p a) :
-    ((l.attachWith p H).map fun i => f i.val) = l.map f :=
-  attachWith_map_coe _ _ _
-
-@[simp]
-theorem attachWith_map_subtype_val {p : α → Prop} (l : Array α) (H : ∀ a ∈ l, p a) :
-    (l.attachWith p H).map Subtype.val = l := by
-  cases l; simp
-
-@[simp]
-theorem mem_attach (l : Array α) : ∀ x, x ∈ l.attach
-  | ⟨a, h⟩ => by
-    have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)
-    rcases this with ⟨⟨_, _⟩, m, rfl⟩
-    exact m
-
-@[simp]
-theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H b} :
-    b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b := by
-  simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm]
-
-theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {l H} {a} (h : a ∈ l) :
-    f a (H a h) ∈ pmap f l H := by
-  rw [mem_pmap]
-  exact ⟨a, h, rfl⟩
-
-@[simp]
-theorem size_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : (pmap f l H).size = l.size := by
-  cases l; simp
-
-@[simp]
-theorem size_attach {L : Array α} : L.attach.size = L.size := by
-  cases L; simp
-
-@[simp]
-theorem size_attachWith {p : α → Prop} {l : Array α} {H} : (l.attachWith p H).size = l.size := by
-  cases l; simp
-
-@[simp]
-theorem pmap_eq_empty_iff {p : α → Prop} {f : ∀ a, p a → β} {l H} : pmap f l H = #[] ↔ l = #[] := by
-  cases l; simp
-
-theorem pmap_ne_empty_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : Array α}
-    (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ #[] ↔ xs ≠ #[] := by
-  cases xs; simp
-
-theorem pmap_eq_self {l : Array α} {p : α → Prop} (hp : ∀ (a : α), a ∈ l → p a)
-    (f : (a : α) → p a → α) : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a := by
-  cases l; simp [List.pmap_eq_self]
-
-@[simp]
-theorem attach_eq_empty_iff {l : Array α} : l.attach = #[] ↔ l = #[] := by
-  cases l; simp
-
-theorem attach_ne_empty_iff {l : Array α} : l.attach ≠ #[] ↔ l ≠ #[] := by
-  cases l; simp
-
-@[simp]
-theorem attachWith_eq_empty_iff {l : Array α} {P : α → Prop} {H : ∀ a ∈ l, P a} :
-    l.attachWith P H = #[] ↔ l = #[] := by
-  cases l; simp
-
-theorem attachWith_ne_empty_iff {l : Array α} {P : α → Prop} {H : ∀ a ∈ l, P a} :
-    l.attachWith P H ≠ #[] ↔ l ≠ #[] := by
-  cases l; simp
-
-@[simp]
-theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Array α} (h : ∀ a ∈ l, p a) (n : Nat) :
-    (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (mem_of_getElem? H) := by
-  cases l; simp
-
-@[simp]
-theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Array α} (h : ∀ a ∈ l, p a) {n : Nat}
-    (hn : n < (pmap f l h).size) :
-    (pmap f l h)[n] =
-      f (l[n]'(@size_pmap _ _ p f l h ▸ hn))
-        (h _ (getElem_mem (@size_pmap _ _ p f l h ▸ hn))) := by
-  cases l; simp
-
-@[simp]
-theorem getElem?_attachWith {xs : Array α} {i : Nat} {P : α → Prop} {H : ∀ a ∈ xs, P a} :
-    (xs.attachWith P H)[i]? = xs[i]?.pmap Subtype.mk (fun _ a => H _ (mem_of_getElem? a)) :=
-  getElem?_pmap ..
-
-@[simp]
-theorem getElem?_attach {xs : Array α} {i : Nat} :
-    xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => mem_of_getElem? a) :=
-  getElem?_attachWith
-
-@[simp]
-theorem getElem_attachWith {xs : Array α} {P : α → Prop} {H : ∀ a ∈ xs, P a}
-    {i : Nat} (h : i < (xs.attachWith P H).size) :
-    (xs.attachWith P H)[i] = ⟨xs[i]'(by simpa using h), H _ (getElem_mem (by simpa using h))⟩ :=
-  getElem_pmap ..
-
-@[simp]
-theorem getElem_attach {xs : Array α} {i : Nat} (h : i < xs.attach.size) :
-    xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
-  getElem_attachWith h
-
-theorem foldl_pmap (l : Array α) {P : α → Prop} (f : (a : α) → P a → β)
-  (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
-    (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
-  rw [pmap_eq_map_attach, foldl_map]
-
-theorem foldr_pmap (l : Array α) {P : α → Prop} (f : (a : α) → P a → β)
-  (H : ∀ (a : α), a ∈ l → P a) (g : β → γ → γ) (x : γ) :
-    (l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
-  rw [pmap_eq_map_attach, foldr_map]
-
-/--
-If we fold over `l.attach` with a function that ignores the membership predicate,
-we get the same results as folding over `l` directly.
-
-This is useful when we need to use `attach` to show termination.
-
-Unfortunately this can't be applied by `simp` because of the higher order unification problem,
-and even when rewriting we need to specify the function explicitly.
-See however `foldl_subtype` below.
--/
-theorem foldl_attach (l : Array α) (f : β → α → β) (b : β) :
-    l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
-  rcases l with ⟨l⟩
-  simp only [List.attach_toArray, List.attachWith_mem_toArray, List.map_attach, size_toArray,
-    List.length_pmap, List.foldl_toArray', mem_toArray, List.foldl_subtype]
-  congr
-  ext
-  simpa using fun a => List.mem_of_getElem? a
-
-/--
-If we fold over `l.attach` with a function that ignores the membership predicate,
-we get the same results as folding over `l` directly.
-
-This is useful when we need to use `attach` to show termination.
-
-Unfortunately this can't be applied by `simp` because of the higher order unification problem,
-and even when rewriting we need to specify the function explicitly.
-See however `foldr_subtype` below.
--/
-theorem foldr_attach (l : Array α) (f : α → β → β) (b : β) :
-    l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
-  rcases l with ⟨l⟩
-  simp only [List.attach_toArray, List.attachWith_mem_toArray, List.map_attach, size_toArray,
-    List.length_pmap, List.foldr_toArray', mem_toArray, List.foldr_subtype]
-  congr
-  ext
-  simpa using fun a => List.mem_of_getElem? a
-
-theorem attach_map {l : Array α} (f : α → β) :
-    (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
-  cases l
-  ext <;> simp
-
-theorem attachWith_map {l : Array α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ l.map f → P b} :
-    (l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
-      fun ⟨x, h⟩ => ⟨f x, h⟩ := by
-  cases l
-  ext
-  · simp
-  · simp only [List.map_toArray, List.attachWith_toArray, List.getElem_toArray,
-      List.getElem_attachWith, List.getElem_map, Function.comp_apply]
-    erw [List.getElem_attachWith] -- Why is `erw` needed here?
-
-theorem map_attachWith {l : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
-    (f : { x // P x } → β) :
-    (l.attachWith P H).map f =
-      l.pmap (fun a (h : a ∈ l ∧ P a) => f ⟨a, H _ h.1⟩) (fun a h => ⟨h, H a h⟩) := by
-  cases l
-  ext <;> simp
-
-/-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`. -/
-theorem map_attach {l : Array α} (f : { x // x ∈ l } → β) :
-    l.attach.map f = l.pmap (fun a h => f ⟨a, h⟩) (fun _ => id) := by
-  cases l
-  ext <;> simp
-
-theorem attach_filterMap {l : Array α} {f : α → Option β} :
-    (l.filterMap f).attach = l.attach.filterMap
-      fun ⟨x, h⟩ => (f x).pbind (fun b m => some ⟨b, mem_filterMap.mpr ⟨x, h, m⟩⟩) := by
-  cases l
-  rw [attach_congr (List.filterMap_toArray f _)]
-  simp [List.attach_filterMap, List.map_filterMap, Function.comp_def]
-
-theorem attach_filter {l : Array α} (p : α → Bool) :
-    (l.filter p).attach = l.attach.filterMap
-      fun x => if w : p x.1 then some ⟨x.1, mem_filter.mpr ⟨x.2, w⟩⟩ else none := by
-  cases l
-  rw [attach_congr (List.filter_toArray p _)]
-  simp [List.attach_filter, List.map_filterMap, Function.comp_def]
-
--- We are still missing here `attachWith_filterMap` and `attachWith_filter`.
--- Also missing are `filterMap_attach`, `filter_attach`, `filterMap_attachWith` and `filter_attachWith`.
-
-theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l H₁ H₂) :
-    pmap f (pmap g l H₁) H₂ =
-      pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
-        (fun a _ => H₁ a a.2) := by
-  cases l
-  simp [List.pmap_pmap, List.pmap_map]
-
-@[simp] theorem pmap_append {p : ι → Prop} (f : ∀ a : ι, p a → α) (l₁ l₂ : Array ι)
-    (h : ∀ a ∈ l₁ ++ l₂, p a) :
-    (l₁ ++ l₂).pmap f h =
-      (l₁.pmap f fun a ha => h a (mem_append_left l₂ ha)) ++
-        l₂.pmap f fun a ha => h a (mem_append_right l₁ ha) := by
-  cases l₁
-  cases l₂
-  simp
-
-theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ l₂ : Array α)
-    (h₁ : ∀ a ∈ l₁, p a) (h₂ : ∀ a ∈ l₂, p a) :
-    ((l₁ ++ l₂).pmap f fun a ha => (mem_append.1 ha).elim (h₁ a) (h₂ a)) =
-      l₁.pmap f h₁ ++ l₂.pmap f h₂ :=
-  pmap_append f l₁ l₂ _
-
-@[simp] theorem attach_append (xs ys : Array α) :
-    (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_left ys h⟩) ++
-      ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_right xs h⟩ := by
-  cases xs
-  cases ys
-  rw [attach_congr (List.append_toArray _ _)]
-  simp [List.attach_append, Function.comp_def]
-
-@[simp] theorem attachWith_append {P : α → Prop} {xs ys : Array α}
-    {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
-    (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
-      ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
-  simp [attachWith, attach_append, map_pmap, pmap_append]
-
-@[simp] theorem pmap_reverse {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
-    (H : ∀ (a : α), a ∈ xs.reverse → P a) :
-    xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
-  induction xs <;> simp_all
-
-theorem reverse_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
-    (H : ∀ (a : α), a ∈ xs → P a) :
-    (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
-  rw [pmap_reverse]
-
-@[simp] theorem attachWith_reverse {P : α → Prop} {xs : Array α}
-    {H : ∀ (a : α), a ∈ xs.reverse → P a} :
-    xs.reverse.attachWith P H =
-      (xs.attachWith P (fun a h => H a (by simpa using h))).reverse := by
-  cases xs
-  simp
-
-theorem reverse_attachWith {P : α → Prop} {xs : Array α}
-    {H : ∀ (a : α), a ∈ xs → P a} :
-    (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) := by
-  cases xs
-  simp
-
-@[simp] theorem attach_reverse (xs : Array α) :
-    xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
-  cases xs
-  rw [attach_congr (List.reverse_toArray _)]
-  simp
-
-theorem reverse_attach (xs : Array α) :
-    xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
-  cases xs
-  simp
-
-@[simp] theorem back?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
-    (H : ∀ (a : α), a ∈ xs → P a) :
-    (xs.pmap f H).back? = xs.attach.back?.map fun ⟨a, m⟩ => f a (H a m) := by
-  cases xs
-  simp
-
-@[simp] theorem back?_attachWith {P : α → Prop} {xs : Array α}
-    {H : ∀ (a : α), a ∈ xs → P a} :
-    (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back?_eq_some h)⟩) := by
-  cases xs
-  simp
-
-@[simp]
-theorem back?_attach {xs : Array α} :
-    xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back?_eq_some h⟩ := by
-  cases xs
-  simp
-
 /-! ## unattach
 
 `Array.unattach` is the (one-sided) inverse of `Array.attach`. It is a synonym for `Array.map Subtype.val`.
@@ -487,15 +128,6 @@ def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) := l.map (
   cases l
   simp
 
-@[simp] theorem getElem?_unattach {p : α → Prop} {l : Array { x // p x }} (i : Nat) :
-    l.unattach[i]? = l[i]?.map Subtype.val := by
-  simp [unattach]
-
-@[simp] theorem getElem_unattach
-    {p : α → Prop} {l : Array { x // p x }} (i : Nat) (h : i < l.unattach.size) :
-    l.unattach[i] = (l[i]'(by simpa using h)).1 := by
-  simp [unattach]
-
 /-! ### Recognizing higher order functions using a function that only depends on the value. -/
 
 /--

src/Init/Data/Array/Basic.lean

@@ -613,15 +613,8 @@ def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
-@[inline]
-def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as.size) :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  loop (j : Nat) :=
-    if h : j < as.size then
-      if p as[j] then some ⟨j, h⟩ else loop (j + 1)
-    else none
-    decreasing_by simp_wf; decreasing_trivial_pre_omega
-  loop 0
+def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
+  a.findIdx? fun a => a == v
 
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
@@ -634,10 +627,6 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega
 def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
   indexOfAux a v 0
 
-@[deprecated indexOf? (since := "2024-11-20")]
-def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
-  a.findIdx? fun a => a == v
-
 @[inline]
 def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
   Id.run <| as.anyM p start stop
@@ -777,62 +766,48 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   go 0 #[]
 
-/--
-Remove the element at a given index from an array without a runtime bounds checks,
-using a `Nat` index and a tactic-provided bound.
+/-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
 
-This function takes worst case O(n) time because
-it has to backshift all elements at positions greater than `i`.-/
+  This function takes worst case O(n) time because
+  it has to backshift all elements at positions greater than `i`.-/
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-def eraseIdx (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α :=
-  if h' : i + 1 < a.size then
-    let a' := a.swap ⟨i + 1, h'⟩ ⟨i, h⟩
-    a'.eraseIdx (i + 1) (by simp [a', h'])
+def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
+  if h : i.val + 1 < a.size then
+    let a' := a.swap ⟨i.val + 1, h⟩ i
+    let i' : Fin a'.size := ⟨i.val + 1, by simp [a', h]⟩
+    a'.feraseIdx i'
   else
     a.pop
-termination_by a.size - i
-decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h
+termination_by a.size - i.val
+decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
 
 -- This is required in `Lean.Data.PersistentHashMap`.
-@[simp] theorem size_eraseIdx (a : Array α) (i : Nat) (h) : (a.eraseIdx i h).size = a.size - 1 := by
-  induction a, i, h using Array.eraseIdx.induct with
-  | @case1 a i h h' a' ih =>
-    unfold eraseIdx
-    simp [h', a', ih]
-  | case2 a i h h' =>
-    unfold eraseIdx
-    simp [h']
+@[simp] theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
+  induction a, i using Array.feraseIdx.induct with
+  | @case1 a i h a' _ ih =>
+    unfold feraseIdx
+    simp [h, a', ih]
+  | case2 a i h =>
+    unfold feraseIdx
+    simp [h]
 
 /-- Remove the element at a given index from an array, or do nothing if the index is out of bounds.
 
   This function takes worst case O(n) time because
   it has to backshift all elements at positions greater than `i`.-/
-def eraseIdxIfInBounds (a : Array α) (i : Nat) : Array α :=
-  if h : i < a.size then a.eraseIdx i h else a
-
-/-- Remove the element at a given index from an array, or panic if the index is out of bounds.
-
-This function takes worst case O(n) time because
-it has to backshift all elements at positions greater than `i`. -/
-def eraseIdx! (a : Array α) (i : Nat) : Array α :=
-  if h : i < a.size then a.eraseIdx i h else panic! "invalid index"
+def eraseIdx (a : Array α) (i : Nat) : Array α :=
+  if h : i < a.size then a.feraseIdx ⟨i, h⟩ else a
 
 def erase [BEq α] (as : Array α) (a : α) : Array α :=
   match as.indexOf? a with
   | none   => as
-  | some i => as.eraseIdx i
-
-/-- Erase the first element that satisfies the predicate `p`. -/
-def eraseP (as : Array α) (p : α → Bool) : Array α :=
-  match as.findIdx? p with
-  | none   => as
-  | some i => as.eraseIdxIfInBounds i
+  | some i => as.feraseIdx i
 
 /-- Insert element `a` at position `i`. -/
-@[inline] def insertIdx (as : Array α) (i : Nat) (a : α) (_ : i ≤ as.size := by get_elem_tactic) : Array α :=
+@[inline] def insertAt (as : Array α) (i : Fin (as.size + 1)) (a : α) : Array α :=
   let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   loop (as : Array α) (j : Fin as.size) :=
-    if i < j then
+    if i.1 < j then
       let j' := ⟨j-1, Nat.lt_of_le_of_lt (Nat.pred_le _) j.2⟩
       let as := as.swap j' j
       loop as ⟨j', by rw [size_swap]; exact j'.2⟩
@@ -843,23 +818,12 @@ def eraseP (as : Array α) (p : α → Bool) : Array α :=
   let as := as.push a
   loop as ⟨j, size_push .. ▸ j.lt_succ_self⟩
 
-@[deprecated insertIdx (since := "2024-11-20")] abbrev insertAt := @insertIdx
-
 /-- Insert element `a` at position `i`. Panics if `i` is not `i ≤ as.size`. -/
-def insertIdx! (as : Array α) (i : Nat) (a : α) : Array α :=
+def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
   if h : i ≤ as.size then
-    insertIdx as i a
+    insertAt as ⟨i, Nat.lt_succ_of_le h⟩ a
   else panic! "invalid index"
 
-@[deprecated insertIdx! (since := "2024-11-20")] abbrev insertAt! := @insertIdx!
-
-/-- Insert element `a` at position `i`, or do nothing if `as.size < i`. -/
-def insertIdxIfInBounds (as : Array α) (i : Nat) (a : α) : Array α :=
-  if h : i ≤ as.size then
-    insertIdx as i a
-  else
-    as
-
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then

src/Init/Data/Array/BinSearch.lean

@@ -52,7 +52,7 @@ namespace Array
     let mid    := (lo + hi)/2
     let midVal := as.get! mid
     if lt midVal k then
-      if mid == lo then do let v ← add (); pure <| as.insertIdx! (lo+1) v
+      if mid == lo then do let v ← add (); pure <| as.insertAt! (lo+1) v
       else binInsertAux lt merge add as k mid hi
     else if lt k midVal then
       binInsertAux lt merge add as k lo mid
@@ -67,7 +67,7 @@ namespace Array
     (k : α) : m (Array α) :=
   let _ := Inhabited.mk k
   if as.isEmpty then do let v ← add (); pure <| as.push v
-  else if lt k (as.get! 0) then do let v ← add (); pure <| as.insertIdx! 0 v
+  else if lt k (as.get! 0) then do let v ← add (); pure <| as.insertAt! 0 v
   else if !lt (as.get! 0) k then as.modifyM 0 <| merge
   else if lt as.back! k then do let v ← add (); pure <| as.push v
   else if !lt k as.back! then as.modifyM (as.size - 1) <| merge

src/Init/Data/Array/Find.lean

@@ -272,10 +272,4 @@ theorem find?_mkArray_eq_none {n : Nat} {a : α} {p : α → Bool} :
     ((mkArray n a).find? p).get h = a := by
   simp [mkArray_eq_toArray_replicate]
 
-theorem find?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
-    (H : ∀ (a : α), a ∈ xs → P a) (p : β → Bool) :
-    (xs.pmap f H).find? p = (xs.attach.find? (fun ⟨a, m⟩ => p (f a (H a m)))).map fun ⟨a, m⟩ => f a (H a m) := by
-  simp only [pmap_eq_map_attach, find?_map]
-  rfl
-
 end Array

src/Init/Data/Array/Lemmas.lean

@@ -23,9 +23,6 @@ import Init.TacticsExtra
 
 namespace Array
 
-@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
-  simp [mem_def]
-
 @[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] := rfl
@@ -39,21 +36,12 @@ theorem getElem?_eq_getElem {a : Array α} {i : Nat} (h : i < a.size) : a[i]? =
   · rw [getElem?_neg a i h]
     simp_all
 
-@[simp] theorem none_eq_getElem?_iff {a : Array α} {i : Nat} : none = a[i]? ↔ a.size ≤ i := by
-  simp [eq_comm (a := none)]
-
 theorem getElem?_eq {a : Array α} {i : Nat} :
     a[i]? = if h : i < a.size then some a[i] else none := by
   split
   · simp_all [getElem?_eq_getElem]
   · simp_all
 
-theorem getElem?_eq_some_iff {a : Array α} : a[i]? = some b ↔ ∃ h : i < a.size, a[i] = b := by
-  simp [getElem?_eq]
-
-theorem some_eq_getElem?_iff {a : Array α} : some b = a[i]? ↔ ∃ h : i < a.size, a[i] = b := by
-  rw [eq_comm, getElem?_eq_some_iff]
-
 theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[i]? := by
   rw [getElem?_eq]
   split <;> simp_all
@@ -78,35 +66,6 @@ theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size)
 @[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 mem_push {a : Array α} {x y : α} : x ∈ a.push y ↔ x ∈ a ∨ x = y := by
-  simp [mem_def]
-
-theorem mem_push_self {a : Array α} {x : α} : x ∈ a.push x :=
-  mem_push.2 (Or.inr rfl)
-
-theorem mem_push_of_mem {a : Array α} {x : α} (y : α) (h : x ∈ a) : x ∈ a.push y :=
-  mem_push.2 (Or.inl h)
-
-theorem getElem_of_mem {a} {l : Array α} (h : a ∈ l) : ∃ (n : Nat) (h : n < l.size), l[n]'h = a := by
-  cases l
-  simp [List.getElem_of_mem (by simpa using h)]
-
-theorem getElem?_of_mem {a} {l : Array α} (h : a ∈ l) : ∃ n : Nat, l[n]? = some a :=
-  let ⟨n, _, e⟩ := getElem_of_mem h; ⟨n, e ▸ getElem?_eq_getElem _⟩
-
-theorem mem_of_getElem? {l : Array α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l :=
-  let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..
-
-theorem mem_iff_getElem {a} {l : Array α} : a ∈ l ↔ ∃ (n : Nat) (h : n < l.size), l[n]'h = a :=
-  ⟨getElem_of_mem, fun ⟨_, _, e⟩ => e ▸ getElem_mem ..⟩
-
-theorem mem_iff_getElem? {a} {l : Array α} : a ∈ l ↔ ∃ n : Nat, l[n]? = some a := by
-  simp [getElem?_eq_some_iff, mem_iff_getElem]
-
-theorem forall_getElem {l : Array α} {p : α → Prop} :
-    (∀ (n : Nat) h, p (l[n]'h)) ↔ ∀ a, a ∈ l → p a := by
-  cases l; simp [List.forall_getElem]
-
 @[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
@@ -134,6 +93,9 @@ We prefer to pull `List.toArray` outwards.
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
 
+@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+  simp [mem_def]
+
 @[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
   apply ext'
   simp
@@ -621,7 +583,7 @@ theorem getElem?_ofFn (f : Fin n → α) (i : Nat) :
     (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none := by
   simp [getElem?_def]
 
-/-! # mkArray -/
+/-- # mkArray -/
 
 @[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
   List.length_replicate ..
@@ -637,12 +599,25 @@ theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
     (mkArray n v)[i]? = if i < n then some v else none := by
   simp [getElem?_def]
 
-/-! # mem -/
+/-- # mem -/
 
 @[simp] theorem mem_toList {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l := mem_def.symm
 
 theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
 
+theorem getElem_of_mem {a : α} {as : Array α} :
+    a ∈ as → (∃ (n : Nat) (h : n < as.size), as[n]'h = a) := by
+  intro ha
+  rcases List.getElem_of_mem ha.val with ⟨i, hbound, hi⟩
+  exists i
+  exists hbound
+
+theorem getElem?_of_mem {a : α} {as : Array α} :
+    a ∈ as → ∃ (n : Nat), as[n]? = some a := by
+  intro ha
+  rcases List.getElem?_of_mem ha.val with ⟨i, hi⟩
+  exists i
+
 @[simp] theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p → Array α} :
     (x ∈ if h : p then #[] else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
   split <;> simp_all
@@ -659,7 +634,7 @@ theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
     (x ∈ if p then l else #[]) ↔ p ∧ x ∈ l := by
   split <;> simp_all
 
-/-! # get lemmas -/
+/-- # get lemmas -/
 
 theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size} (_ : a[idx] = x) :
     idx < a.size :=
@@ -684,6 +659,10 @@ theorem get?_eq_get?_toList (a : Array α) (i : Nat) : a.get? i = a.toList.get?
 theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
   simp only [get!_eq_getElem?, get?_eq_getElem?]
 
+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]
+
 theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD default := by
   simp only [back!, get!_eq_getElem?, get?_eq_getElem?, back?]
 
@@ -693,10 +672,6 @@ theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD de
 @[simp] theorem back!_push [Inhabited α] (a : Array α) : (a.push x).back! = x := by
   simp [back!_eq_back?]
 
-theorem mem_of_back?_eq_some {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs := by
-  cases xs
-  simpa using List.mem_of_getLast?_eq_some (by simpa using h)
-
 theorem getElem?_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]
@@ -1050,10 +1025,6 @@ theorem foldr_congr {as bs : Array α} (h₀ : as = bs) {f g : α → β → β}
 @[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
   simp only [mem_def, toList_map, List.mem_map]
 
-theorem exists_of_mem_map (h : b ∈ map f l) : ∃ a, a ∈ l ∧ f a = b := mem_map.1 h
-
-theorem mem_map_of_mem (f : α → β) (h : a ∈ l) : f a ∈ map f l := mem_map.2 ⟨_, h, rfl⟩
-
 theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by
   rw [mapM_eq_foldlM, ← foldlM_toList, ← List.foldrM_reverse]
@@ -1244,12 +1215,6 @@ theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] :=
 @[simp] theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
   simp only [mem_def, toList_append, List.mem_append]
 
-theorem mem_append_left {a : α} {l₁ : Array α} (l₂ : Array α) (h : a ∈ l₁) : a ∈ l₁ ++ l₂ :=
-  mem_append.2 (Or.inl h)
-
-theorem mem_append_right {a : α} (l₁ : Array α) {l₂ : Array α} (h : a ∈ l₂) : a ∈ l₁ ++ l₂ :=
-  mem_append.2 (Or.inr h)
-
 @[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
   simp only [size, toList_append, List.length_append]
 
@@ -1637,9 +1602,9 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
 
 /-! ### eraseIdx -/
 
-theorem eraseIdx_eq_eraseIdxIfInBounds {a : Array α} {i : Nat} (h : i < a.size) :
-    a.eraseIdx i h = a.eraseIdxIfInBounds i := by
-  simp [eraseIdxIfInBounds, h]
+theorem feraseIdx_eq_eraseIdx {a : Array α} {i : Fin a.size} :
+    a.feraseIdx i = a.eraseIdx i.1 := by
+  simp [eraseIdx]
 
 /-! ### isPrefixOf -/
 
@@ -1869,15 +1834,16 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
     l.toArray.takeWhile p = (l.takeWhile p).toArray := by
   simp [Array.takeWhile, takeWhile_go_toArray]
 
-@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) :
-    l.toArray.eraseIdx i h = (l.eraseIdx i).toArray := by
-  rw [Array.eraseIdx]
-  split <;> rename_i h'
-  · rw [eraseIdx_toArray]
+@[simp] theorem feraseIdx_toArray (l : List α) (i : Fin l.toArray.size) :
+    l.toArray.feraseIdx i = (l.eraseIdx i).toArray := by
+  rw [feraseIdx]
+  split <;> rename_i h
+  · rw [feraseIdx_toArray]
     simp only [swap_toArray, Fin.getElem_fin, toList_toArray, mk.injEq]
     rw [eraseIdx_set_gt (by simp), eraseIdx_set_eq]
     simp
-  · simp at h h'
+  · rcases i with ⟨i, w⟩
+    simp at h w
     have t : i = l.length - 1 := by omega
     simp [t]
 termination_by l.length - i
@@ -1887,9 +1853,9 @@ decreasing_by
   simp
   omega
 
-@[simp] theorem eraseIdxIfInBounds_toArray (l : List α) (i : Nat) :
-    l.toArray.eraseIdxIfInBounds i = (l.eraseIdx i).toArray := by
-  rw [Array.eraseIdxIfInBounds]
+@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) :
+    l.toArray.eraseIdx i = (l.eraseIdx i).toArray := by
+  rw [Array.eraseIdx]
   split
   · simp
   · simp_all [eraseIdx_eq_self.2]
@@ -1908,13 +1874,13 @@ namespace Array
     (as.takeWhile p).toList = as.toList.takeWhile p := by
   induction as; simp
 
-@[simp] theorem toList_eraseIdx (as : Array α) (i : Nat) (h : i < as.size) :
-    (as.eraseIdx i h).toList = as.toList.eraseIdx i := by
+@[simp] theorem toList_feraseIdx (as : Array α) (i : Fin as.size) :
+    (as.feraseIdx i).toList = as.toList.eraseIdx i.1 := by
   induction as
   simp
 
-@[simp] theorem toList_eraseIdxIfInBounds (as : Array α) (i : Nat) :
-    (as.eraseIdxIfInBounds i).toList = as.toList.eraseIdx i := by
+@[simp] theorem toList_eraseIdx (as : Array α) (i : Nat) :
+    (as.eraseIdx i).toList = as.toList.eraseIdx i := by
   induction as
   simp
 
@@ -1948,26 +1914,6 @@ theorem array_array_induction (P : Array (Array α) → Prop) (h : ∀ (xss : Li
   specialize h (ass.toList.map toList)
   simpa [← toList_map, Function.comp_def, map_id] using h
 
-theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : Array β₁) (init : α) :
-    (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by
-  cases l; simp [List.foldl_map]
-
-theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : Array α₁) (init : β) :
-    (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
-  cases l; simp [List.foldr_map]
-
-theorem foldl_filterMap (f : α → Option β) (g : γ → β → γ) (l : Array α) (init : γ) :
-    (l.filterMap f).foldl g init = l.foldl (fun x y => match f y with | some b => g x b | none => x) init := by
-  cases l
-  simp [List.foldl_filterMap]
-  rfl
-
-theorem foldr_filterMap (f : α → Option β) (g : β → γ → γ) (l : Array α) (init : γ) :
-    (l.filterMap f).foldr g init = l.foldr (fun x y => match f x with | some b => g b y | none => y) init := by
-  cases l
-  simp [List.foldr_filterMap]
-  rfl
-
 /-! ### flatten -/
 
 @[simp] theorem flatten_empty : flatten (#[] : Array (Array α)) = #[] := rfl
@@ -1982,12 +1928,6 @@ theorem foldr_filterMap (f : α → Option β) (g : β → γ → γ) (l : Array
   | nil => simp
   | cons xs xss ih => simp [ih]
 
-/-! ### reverse -/
-
-@[simp] theorem mem_reverse {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as := by
-  cases as
-  simp
-
 /-! ### findSomeRevM?, findRevM?, findSomeRev?, findRev? -/
 
 @[simp] theorem findSomeRevM?_eq_findSomeM?_reverse

src/Init/Data/BitVec/Lemmas.lean

@@ -2611,7 +2611,7 @@ theorem getLsbD_rotateLeftAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i
   apply getLsbD_ge
   omega
 
-/-- When `r < w`, we give a formula for `(x.rotateLeft r).getLsbD i`. -/
+/-- When `r < w`, we give a formula for `(x.rotateRight r).getLsbD i`. -/
 theorem getLsbD_rotateLeft_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
     (x.rotateLeft r).getLsbD i =
       cond (i < r)
@@ -2638,56 +2638,6 @@ theorem getElem_rotateLeft {x : BitVec w} {r i : Nat} (h : i < w) :
       if h' : i < r % w then x[(w - (r % w) + i)] else x[i - (r % w)] := by
   simp [← BitVec.getLsbD_eq_getElem, h]
 
-/-- If `w ≤ x < 2 * w`, then `x % w = x - w` -/
-theorem mod_eq_sub_of_le_of_lt {x w : Nat} (x_le : w ≤ x) (x_lt : x < 2 * w) :
-    x % w = x - w := by
-  rw [Nat.mod_eq_sub_mod, Nat.mod_eq_of_lt (by omega)]
-  omega
-
-theorem getMsbD_rotateLeftAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) :
-    (x.rotateLeftAux r).getMsbD i = x.getMsbD (r + i) := by
-  rw [rotateLeftAux, getMsbD_or]
-  simp [show i < w - r by omega, Nat.add_comm]
-
-theorem getMsbD_rotateLeftAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ w - r) :
-    (x.rotateLeftAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - (w - r))) := by
-  simp [rotateLeftAux, getMsbD_or, show i + r ≥ w by omega, show ¬i < w - r by omega]
-
-/-- When `r < w`, we give a formula for `(x.rotateLeft r).getMsbD i`. -/
-theorem getMsbD_rotateLeft_of_lt {n w : Nat} {x : BitVec w} (hi : r < w):
-    (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w)) := by
-  rcases w with rfl | w
-  · simp
-  · rw [BitVec.rotateLeft_eq_rotateLeftAux_of_lt (by omega)]
-    by_cases h : n < (w + 1) - r
-    · simp [getMsbD_rotateLeftAux_of_lt h, Nat.mod_eq_of_lt, show r + n < (w + 1) by omega, show n < w + 1 by omega]
-    · simp [getMsbD_rotateLeftAux_of_ge <| Nat.ge_of_not_lt h]
-      by_cases h₁ : n < w + 1
-      · simp only [h₁, decide_true, Bool.true_and]
-        have h₂ : (r + n) < 2 * (w + 1) := by omega
-        rw [mod_eq_sub_of_le_of_lt (by omega) (by omega)]
-        congr 1
-        omega
-      · simp [h₁]
-
-theorem getMsbD_rotateLeft {r n w : Nat} {x : BitVec w} :
-    (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w)) := by
-  rcases w with rfl | w
-  · simp
-  · by_cases h : r < w
-    · rw [getMsbD_rotateLeft_of_lt (by omega)]
-    · rw [← rotateLeft_mod_eq_rotateLeft, getMsbD_rotateLeft_of_lt (by apply Nat.mod_lt; simp)]
-      simp
-
-@[simp]
-theorem msb_rotateLeft {m w : Nat} {x : BitVec w} :
-    (x.rotateLeft m).msb = x.getMsbD (m % w) := by
-  simp only [BitVec.msb, getMsbD_rotateLeft]
-  by_cases h : w = 0
-  · simp [h]
-  · simp
-    omega
-
 /-! ## Rotate Right -/
 
 /--
@@ -2749,7 +2699,7 @@ theorem rotateRight_mod_eq_rotateRight {x : BitVec w} {r : Nat} :
   simp only [rotateRight, Nat.mod_mod]
 
 /-- When `r < w`, we give a formula for `(x.rotateRight r).getLsb i`. -/
-theorem getLsbD_rotateRight_of_lt {x : BitVec w} {r i : Nat} (hr: r < w) :
+theorem getLsbD_rotateRight_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
     (x.rotateRight r).getLsbD i =
       cond (i < w - r)
       (x.getLsbD (r + i))
@@ -2767,7 +2717,7 @@ theorem getLsbD_rotateRight {x : BitVec w} {r i : Nat} :
       (decide (i < w) && x.getLsbD (i - (w - (r % w)))) := by
   rcases w with ⟨rfl, w⟩
   · simp
-  · rw [← rotateRight_mod_eq_rotateRight, getLsbD_rotateRight_of_lt (Nat.mod_lt _ (by omega))]
+  · rw [← rotateRight_mod_eq_rotateRight, getLsbD_rotateRight_of_le (Nat.mod_lt _ (by omega))]
 
 @[simp]
 theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
@@ -2775,56 +2725,6 @@ theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
   simp only [← BitVec.getLsbD_eq_getElem]
   simp [getLsbD_rotateRight, h]
 
-theorem getMsbD_rotateRightAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
-    (x.rotateRightAux r).getMsbD i = x.getMsbD (i + (w - r)) := by
-  rw [rotateRightAux, getMsbD_or, getMsbD_ushiftRight]
-  simp [show i < r by omega]
-
-theorem getMsbD_rotateRightAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ r) :
-    (x.rotateRightAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - r)) := by
-  simp [rotateRightAux, show ¬ i < r by omega, show i + (w - r) ≥ w by omega]
-
-/-- When `m < w`, we give a formula for `(x.rotateLeft m).getMsbD i`. -/
-@[simp]
-theorem getMsbD_rotateRight_of_lt {w n m : Nat} {x : BitVec w} (hr : m < w):
-    (x.rotateRight m).getMsbD n = (decide (n < w) && (if (n < m % w)
-    then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))):= by
-  rcases w with rfl | w
-  · simp
-  · rw [rotateRight_eq_rotateRightAux_of_lt (by omega)]
-    by_cases h : n < m
-    · simp only [getMsbD_rotateRightAux_of_lt h, show n < w + 1 by omega, decide_true,
-        show m % (w + 1) = m by rw [Nat.mod_eq_of_lt hr], h, ↓reduceIte,
-        show (w + 1 + n - m) < (w + 1) by omega, Nat.mod_eq_of_lt, Bool.true_and]
-      congr 1
-      omega
-    · simp [h, getMsbD_rotateRightAux_of_ge <| Nat.ge_of_not_lt h]
-      by_cases h₁ : n < w + 1
-      · simp [h, h₁, decide_true, Bool.true_and, Nat.mod_eq_of_lt hr]
-      · simp [h₁]
-
-@[simp]
-theorem getMsbD_rotateRight {w n m : Nat} {x : BitVec w} :
-    (x.rotateRight m).getMsbD n = (decide (n < w) && (if (n < m % w)
-    then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))):= by
-  rcases w with rfl | w
-  · simp
-  · by_cases h₀ : m < w
-    · rw [getMsbD_rotateRight_of_lt (by omega)]
-    · rw [← rotateRight_mod_eq_rotateRight, getMsbD_rotateRight_of_lt (by apply Nat.mod_lt; simp)]
-      simp
-
-@[simp]
-theorem msb_rotateRight {r w : Nat} {x : BitVec w} :
-    (x.rotateRight r).msb = x.getMsbD ((w - r % w) % w) := by
-  simp only [BitVec.msb, getMsbD_rotateRight]
-  by_cases h₀ : 0 < w
-  · simp only [h₀, decide_true, Nat.add_zero, Nat.zero_le, Nat.sub_eq_zero_of_le, Bool.true_and,
-    ite_eq_left_iff, Nat.not_lt, Nat.le_zero_eq]
-    intro h₁
-    simp [h₁]
-  · simp [show w = 0 by omega]
-
 /- ## twoPow -/
 
 theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by

src/Init/Data/Float.lean

@@ -31,7 +31,7 @@ opaque floatSpec : FloatSpec := {
 structure Float where
   val : floatSpec.float
 
-instance : Nonempty Float := ⟨{ val := floatSpec.val }⟩
+instance : Inhabited Float := ⟨{ val := floatSpec.val }⟩
 
 @[extern "lean_float_add"] opaque Float.add : Float → Float → Float
 @[extern "lean_float_sub"] opaque Float.sub : Float → Float → Float
@@ -136,9 +136,6 @@ instance : ToString Float where
 
 @[extern "lean_uint64_to_float"] opaque UInt64.toFloat (n : UInt64) : Float
 
-instance : Inhabited Float where
-  default := UInt64.toFloat 0
-
 instance : Repr Float where
   reprPrec n prec := if n < UInt64.toFloat 0 then Repr.addAppParen (toString n) prec else toString n
 

src/Init/Data/List/Attach.lean

@@ -13,7 +13,7 @@ namespace List
   `a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l`
   but is defined only when all members of `l` satisfy `P`, using the proof
   to apply `f`. -/
-def pmap {P : α → Prop} (f : ∀ a, P a → β) : ∀ l : List α, (H : ∀ a ∈ l, P a) → List β
+@[simp] def pmap {P : α → Prop} (f : ∀ a, P a → β) : ∀ l : List α, (H : ∀ a ∈ l, P a) → List β
   | [], _ => []
   | a :: l, H => f a (forall_mem_cons.1 H).1 :: pmap f l (forall_mem_cons.1 H).2
 
@@ -46,11 +46,6 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
   | cons _ L', hL' => congrArg _ <| go L' fun _ hx => hL' (.tail _ hx)
   exact go L h'
 
-@[simp] theorem pmap_nil {P : α → Prop} (f : ∀ a, P a → β) : pmap f [] (by simp) = [] := rfl
-
-@[simp] theorem pmap_cons {P : α → Prop} (f : ∀ a, P a → β) (a : α) (l : List α) (h : ∀ b ∈ a :: l, P b) :
-    pmap f (a :: l) h = f a (forall_mem_cons.1 h).1 :: pmap f l (forall_mem_cons.1 h).2 := rfl
-
 @[simp] theorem attach_nil : ([] : List α).attach = [] := rfl
 
 @[simp] theorem attachWith_nil : ([] : List α).attachWith P H = [] := rfl
@@ -153,7 +148,7 @@ theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {l H} {a} (h :
   exact ⟨a, h, rfl⟩
 
 @[simp]
-theorem length_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : (pmap f l H).length = l.length := by
+theorem length_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : length (pmap f l H) = length l := by
   induction l
   · rfl
   · simp only [*, pmap, length]
@@ -204,7 +199,7 @@ theorem attachWith_ne_nil_iff {l : List α} {P : α → Prop} {H : ∀ a ∈ l,
 
 @[simp]
 theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) :
-    (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (mem_of_getElem? H) := by
+    (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (getElem?_mem H) := by
   induction l generalizing n with
   | nil => simp
   | cons hd tl hl =>
@@ -220,7 +215,7 @@ theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h
       · simp_all
 
 theorem get?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) :
-    get? (pmap f l h) n = Option.pmap f (get? l n) fun x H => h x (mem_of_get? H) := by
+    get? (pmap f l h) n = Option.pmap f (get? l n) fun x H => h x (get?_mem H) := by
   simp only [get?_eq_getElem?]
   simp [getElem?_pmap, h]
 
@@ -243,18 +238,18 @@ theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h :
     (hn : n < (pmap f l h).length) :
     get (pmap f l h) ⟨n, hn⟩ =
       f (get l ⟨n, @length_pmap _ _ p f l h ▸ hn⟩)
-        (h _ (getElem_mem (@length_pmap _ _ p f l h ▸ hn))) := by
+        (h _ (get_mem l n (@length_pmap _ _ p f l h ▸ hn))) := by
   simp only [get_eq_getElem]
   simp [getElem_pmap]
 
 @[simp]
 theorem getElem?_attachWith {xs : List α} {i : Nat} {P : α → Prop} {H : ∀ a ∈ xs, P a} :
-    (xs.attachWith P H)[i]? = xs[i]?.pmap Subtype.mk (fun _ a => H _ (mem_of_getElem? a)) :=
+    (xs.attachWith P H)[i]? = xs[i]?.pmap Subtype.mk (fun _ a => H _ (getElem?_mem a)) :=
   getElem?_pmap ..
 
 @[simp]
 theorem getElem?_attach {xs : List α} {i : Nat} :
-    xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => mem_of_getElem? a) :=
+    xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => getElem?_mem a) :=
   getElem?_attachWith
 
 @[simp]
@@ -338,7 +333,6 @@ This is useful when we need to use `attach` to show termination.
 
 Unfortunately this can't be applied by `simp` because of the higher order unification problem,
 and even when rewriting we need to specify the function explicitly.
-See however `foldl_subtype` below.
 -/
 theorem foldl_attach (l : List α) (f : β → α → β) (b : β) :
     l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
@@ -354,7 +348,6 @@ This is useful when we need to use `attach` to show termination.
 
 Unfortunately this can't be applied by `simp` because of the higher order unification problem,
 and even when rewriting we need to specify the function explicitly.
-See however `foldr_subtype` below.
 -/
 theorem foldr_attach (l : List α) (f : α → β → β) (b : β) :
     l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
@@ -459,16 +452,16 @@ theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ l₂ :
   pmap_append f l₁ l₂ _
 
 @[simp] theorem attach_append (xs ys : List α) :
-    (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_left ys h⟩) ++
-      ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_right xs h⟩ := by
+    (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_of_mem_left ys h⟩) ++
+      ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_of_mem_right xs h⟩ := by
   simp only [attach, attachWith, pmap, map_pmap, pmap_append]
   congr 1 <;>
   exact pmap_congr_left _ fun _ _ _ _ => rfl
 
 @[simp] theorem attachWith_append {P : α → Prop} {xs ys : List α}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
-    (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
-      ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
+    (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_of_mem_left ys h)) ++
+      ys.attachWith P (fun a h => H a (mem_append_of_mem_right xs h)) := by
   simp only [attachWith, attach_append, map_pmap, pmap_append]
 
 @[simp] theorem pmap_reverse {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
@@ -605,15 +598,6 @@ def unattach {α : Type _} {p : α → Prop} (l : List { x // p x }) := l.map (
   | nil => simp
   | cons a l ih => simp [ih, Function.comp_def]
 
-@[simp] theorem getElem?_unattach {p : α → Prop} {l : List { x // p x }} (i : Nat) :
-    l.unattach[i]? = l[i]?.map Subtype.val := by
-  simp [unattach]
-
-@[simp] theorem getElem_unattach
-    {p : α → Prop} {l : List { x // p x }} (i : Nat) (h : i < l.unattach.length) :
-    l.unattach[i] = (l[i]'(by simpa using h)).1 := by
-  simp [unattach]
-
 /-! ### Recognizing higher order functions on subtypes using a function that only depends on the value. -/
 
 /--

src/Init/Data/List/Basic.lean

@@ -726,13 +726,13 @@ theorem elem_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : List α} (h :
 instance [BEq α] [LawfulBEq α] (a : α) (as : List α) : Decidable (a ∈ as) :=
   decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
 
-theorem mem_append_left {a : α} {as : List α} (bs : List α) : a ∈ as → a ∈ as ++ bs := by
+theorem mem_append_of_mem_left {a : α} {as : List α} (bs : List α) : a ∈ as → a ∈ as ++ bs := by
   intro h
   induction h with
   | head => apply Mem.head
   | tail => apply Mem.tail; assumption
 
-theorem mem_append_right {b : α} {bs : List α} (as : List α) : b ∈ bs → b ∈ as ++ bs := by
+theorem mem_append_of_mem_right {b : α} {bs : List α} (as : List α) : b ∈ bs → b ∈ as ++ bs := by
   intro h
   induction as with
   | nil  => simp [h]

src/Init/Data/List/Control.lean

@@ -256,7 +256,7 @@ theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] (p : α → m Bool) (as :
       have : a ∈ as := by
         have ⟨bs, h⟩ := h
         subst h
-        exact mem_append_right _ (Mem.head ..)
+        exact mem_append_of_mem_right _ (Mem.head ..)
       match (← f a this b) with
       | ForInStep.done b  => pure b
       | ForInStep.yield b =>

src/Init/Data/List/Lemmas.lean

@@ -394,9 +394,9 @@ theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = s
 theorem mem_cons_self (a : α) (l : List α) : a ∈ a :: l := .head ..
 
 theorem mem_concat_self (xs : List α) (a : α) : a ∈ xs ++ [a] :=
-  mem_append_right xs (mem_cons_self a _)
+  mem_append_of_mem_right xs (mem_cons_self a _)
 
-theorem mem_append_cons_self : a ∈ xs ++ a :: ys := mem_append_right _ (mem_cons_self _ _)
+theorem mem_append_cons_self : a ∈ xs ++ a :: ys := mem_append_of_mem_right _ (mem_cons_self _ _)
 
 theorem eq_append_cons_of_mem {a : α} {xs : List α} (h : a ∈ xs) :
     ∃ as bs, xs = as ++ a :: bs ∧ a ∉ as := by
@@ -503,20 +503,16 @@ theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = s
 theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
   let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩
 
-theorem get_mem : ∀ (l : List α) n, get l n ∈ l
-  | _ :: _, ⟨0, _⟩ => .head ..
-  | _ :: l, ⟨_+1, _⟩ => .tail _ (get_mem l ..)
+theorem get_mem : ∀ (l : List α) n h, get l ⟨n, h⟩ ∈ l
+  | _ :: _, 0, _ => .head ..
+  | _ :: l, _+1, _ => .tail _ (get_mem l ..)
 
-theorem mem_of_getElem? {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l :=
+theorem getElem?_mem {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l :=
   let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..
 
-@[deprecated mem_of_getElem? (since := "2024-09-06")] abbrev getElem?_mem := @mem_of_getElem?
-
-theorem mem_of_get? {l : List α} {n a} (e : l.get? n = some a) : a ∈ l :=
+theorem get?_mem {l : List α} {n a} (e : l.get? n = some a) : a ∈ l :=
   let ⟨_, e⟩ := get?_eq_some.1 e; e ▸ get_mem ..
 
-@[deprecated mem_of_get? (since := "2024-09-06")] abbrev get?_mem := @mem_of_get?
-
 theorem mem_iff_getElem {a} {l : List α} : a ∈ l ↔ ∃ (n : Nat) (h : n < l.length), l[n]'h = a :=
   ⟨getElem_of_mem, fun ⟨_, _, e⟩ => e ▸ getElem_mem ..⟩
 
@@ -2001,8 +1997,11 @@ theorem not_mem_append {a : α} {s t : List α} (h₁ : a ∉ s) (h₂ : a ∉ t
 theorem mem_append_eq (a : α) (s t : List α) : (a ∈ s ++ t) = (a ∈ s ∨ a ∈ t) :=
   propext mem_append
 
-@[deprecated mem_append_left (since := "2024-11-20")] abbrev mem_append_of_mem_left := @mem_append_left
-@[deprecated mem_append_right (since := "2024-11-20")] abbrev mem_append_of_mem_right := @mem_append_right
+theorem mem_append_left {a : α} {l₁ : List α} (l₂ : List α) (h : a ∈ l₁) : a ∈ l₁ ++ l₂ :=
+  mem_append.2 (Or.inl h)
+
+theorem mem_append_right {a : α} (l₁ : List α) {l₂ : List α} (h : a ∈ l₂) : a ∈ l₁ ++ l₂ :=
+  mem_append.2 (Or.inr h)
 
 theorem mem_iff_append {a : α} {l : List α} : a ∈ l ↔ ∃ s t : List α, l = s ++ a :: t :=
   ⟨append_of_mem, fun ⟨s, t, e⟩ => e ▸ by simp⟩
@@ -2416,7 +2415,7 @@ theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
 
 @[simp] theorem getElem_replicate (a : α) {n : Nat} {m} (h : m < (replicate n a).length) :
     (replicate n a)[m] = a :=
-  eq_of_mem_replicate (getElem_mem _)
+  eq_of_mem_replicate (get_mem _ _ _)
 
 @[deprecated getElem_replicate (since := "2024-06-12")]
 theorem get_replicate (a : α) {n : Nat} (m : Fin _) : (replicate n a).get m = a := by

src/Init/Data/List/Sublist.lean

@@ -417,7 +417,7 @@ theorem Sublist.of_sublist_append_left (w : ∀ a, a ∈ l → a ∉ l₂) (h :
   obtain ⟨l₁', l₂', rfl, h₁, h₂⟩ := h
   have : l₂' = [] := by
     rw [eq_nil_iff_forall_not_mem]
-    exact fun x m => w x (mem_append_right l₁' m) (h₂.mem m)
+    exact fun x m => w x (mem_append_of_mem_right l₁' m) (h₂.mem m)
   simp_all
 
 theorem Sublist.of_sublist_append_right (w : ∀ a, a ∈ l → a ∉ l₁) (h : l <+ l₁ ++ l₂) : l <+ l₂ := by
@@ -425,7 +425,7 @@ theorem Sublist.of_sublist_append_right (w : ∀ a, a ∈ l → a ∉ l₁) (h :
   obtain ⟨l₁', l₂', rfl, h₁, h₂⟩ := h
   have : l₁' = [] := by
     rw [eq_nil_iff_forall_not_mem]
-    exact fun x m => w x (mem_append_left l₂' m) (h₁.mem m)
+    exact fun x m => w x (mem_append_of_mem_left l₂' m) (h₁.mem m)
   simp_all
 
 theorem Sublist.middle {l : List α} (h : l <+ l₁ ++ l₂) (a : α) : l <+ l₁ ++ a :: l₂ := by

src/Init/Data/Random.lean

@@ -113,10 +113,10 @@ initialize IO.stdGenRef : IO.Ref StdGen ←
   let seed := UInt64.toNat (ByteArray.toUInt64LE! (← IO.getRandomBytes 8))
   IO.mkRef (mkStdGen seed)
 
-def IO.setRandSeed (n : Nat) : BaseIO Unit :=
+def IO.setRandSeed (n : Nat) : IO Unit :=
   IO.stdGenRef.set (mkStdGen n)
 
-def IO.rand (lo hi : Nat) : BaseIO Nat := do
+def IO.rand (lo hi : Nat) : IO Nat := do
   let gen ← IO.stdGenRef.get
   let (r, gen) := randNat gen lo hi
   IO.stdGenRef.set gen

src/Init/Meta.lean

@@ -374,9 +374,6 @@ partial def structEq : Syntax → Syntax → Bool
 instance : BEq Lean.Syntax := ⟨structEq⟩
 instance : BEq (Lean.TSyntax k) := ⟨(·.raw == ·.raw)⟩
 
-/--
-Finds the first `SourceInfo` from the back of `stx` or `none` if no `SourceInfo` can be found.
--/
 partial def getTailInfo? : Syntax → Option SourceInfo
   | atom info _   => info
   | ident info .. => info
@@ -385,39 +382,14 @@ partial def getTailInfo? : Syntax → Option SourceInfo
   | node info _ _    => info
   | _             => none
 
-/--
-Finds the first `SourceInfo` from the back of `stx` or `SourceInfo.none`
-if no `SourceInfo` can be found.
--/
 def getTailInfo (stx : Syntax) : SourceInfo :=
   stx.getTailInfo?.getD SourceInfo.none
 
-/--
-Finds the trailing size of the first `SourceInfo` from the back of `stx`.
-If no `SourceInfo` can be found or the first `SourceInfo` from the back of `stx` contains no
-trailing whitespace, the result is `0`.
--/
 def getTrailingSize (stx : Syntax) : Nat :=
   match stx.getTailInfo? with
   | some (SourceInfo.original (trailing := trailing) ..) => trailing.bsize
   | _ => 0
 
-/--
-Finds the trailing whitespace substring of the first `SourceInfo` from the back of `stx`.
-If no `SourceInfo` can be found or the first `SourceInfo` from the back of `stx` contains
-no trailing whitespace, the result is `none`.
--/
-def getTrailing? (stx : Syntax) : Option Substring :=
-  stx.getTailInfo.getTrailing?
-
-/--
-Finds the tail position of the trailing whitespace of the first `SourceInfo` from the back of `stx`.
-If no `SourceInfo` can be found or the first `SourceInfo` from the back of `stx` contains
-no trailing whitespace and lacks a tail position, the result is `none`.
--/
-def getTrailingTailPos? (stx : Syntax) (canonicalOnly := false) : Option String.Pos :=
-  stx.getTailInfo.getTrailingTailPos? canonicalOnly
-
 /--
   Return substring of original input covering `stx`.
   Result is meaningful only if all involved `SourceInfo.original`s refer to the same string (as is the case after parsing). -/
@@ -431,20 +403,21 @@ def getSubstring? (stx : Syntax) (withLeading := true) (withTrailing := true) :
     }
   | _, _ => none
 
-@[specialize] private partial def updateLast {α} (a : Array α) (f : α → Option α) (i : Fin (a.size + 1)) : Option (Array α) :=
-  match i with
-  | 0 => none
-  | ⟨i + 1, h⟩ =>
-    let v := a[i]'(Nat.succ_lt_succ_iff.mp h)
+@[specialize] private partial def updateLast {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) :=
+  if i == 0 then
+    none
+  else
+    let i := i - 1
+    let v := a[i]!
     match f v with
-    | some v => some <| a.set i v (Nat.succ_lt_succ_iff.mp h)
-    | none   => updateLast a f ⟨i, Nat.lt_of_succ_lt h⟩
+    | some v => some <| a.set! i v
+    | none   => updateLast a f i
 
 partial def setTailInfoAux (info : SourceInfo) : Syntax → Option Syntax
   | atom _ val             => some <| atom info val
   | ident _ rawVal val pre => some <| ident info rawVal val pre
   | node info' k args      =>
-    match updateLast args (setTailInfoAux info) ⟨args.size, by simp⟩ with
+    match updateLast args (setTailInfoAux info) args.size with
     | some args => some <| node info' k args
     | none      => none
   | _                      => none

src/Init/NotationExtra.lean

@@ -22,28 +22,28 @@ syntax explicitBinders            := (ppSpace bracketedExplicitBinders)+ <|> unb
 
 open TSyntax.Compat in
 def expandExplicitBindersAux (combinator : Syntax) (idents : Array Syntax) (type? : Option Syntax) (body : Syntax) : MacroM Syntax :=
-  let rec loop (i : Nat) (h : i ≤ idents.size) (acc : Syntax) := do
+  let rec loop (i : Nat) (acc : Syntax) := do
     match i with
     | 0   => pure acc
-    | i + 1 =>
-      let ident := idents[i][0]
+    | i+1 =>
+      let ident := idents[i]![0]
       let acc ← match ident.isIdent, type? with
         | true,  none      => `($combinator fun $ident => $acc)
         | true,  some type => `($combinator fun $ident : $type => $acc)
         | false, none      => `($combinator fun _ => $acc)
         | false, some type => `($combinator fun _ : $type => $acc)
-      loop i (Nat.le_of_succ_le h) acc
-  loop idents.size (by simp) body
+      loop i acc
+  loop idents.size body
 
 def expandBrackedBindersAux (combinator : Syntax) (binders : Array Syntax) (body : Syntax) : MacroM Syntax :=
-  let rec loop (i : Nat) (h : i ≤ binders.size) (acc : Syntax) := do
+  let rec loop (i : Nat) (acc : Syntax) := do
     match i with
     | 0   => pure acc
     | i+1 =>
-      let idents := binders[i][1].getArgs
-      let type   := binders[i][3]
-      loop i (Nat.le_of_succ_le h) (← expandExplicitBindersAux combinator idents (some type) acc)
-  loop binders.size (by simp) body
+      let idents := binders[i]![1].getArgs
+      let type   := binders[i]![3]
+      loop i (← expandExplicitBindersAux combinator idents (some type) acc)
+  loop binders.size body
 
 def expandExplicitBinders (combinatorDeclName : Name) (explicitBinders : Syntax) (body : Syntax) : MacroM Syntax := do
   let combinator := mkCIdentFrom (← getRef) combinatorDeclName

src/Init/Prelude.lean

@@ -3654,8 +3654,7 @@ namespace SourceInfo
 
 /--
 Gets the position information from a `SourceInfo`, if available.
-If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false`
-will also return `none`.
+If `originalOnly` is true, then `.synthetic` syntax will also return `none`.
 -/
 def getPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
   match info, canonicalOnly with
@@ -3666,8 +3665,7 @@ def getPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
 
 /--
 Gets the end position information from a `SourceInfo`, if available.
-If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false`
-will also return `none`.
+If `originalOnly` is true, then `.synthetic` syntax will also return `none`.
 -/
 def getTailPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
   match info, canonicalOnly with
@@ -3676,24 +3674,6 @@ def getTailPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos
   | synthetic (endPos := endPos) .., false => some endPos
   | _,                               _     => none
 
-/--
-Gets the substring representing the trailing whitespace of a `SourceInfo`, if available.
--/
-def getTrailing? (info : SourceInfo) : Option Substring :=
-  match info with
-  | original (trailing := trailing) .. => some trailing
-  | _                                  => none
-
-/--
-Gets the end position information of the trailing whitespace of a `SourceInfo`, if available.
-If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false`
-will also return `none`.
--/
-def getTrailingTailPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
-  match info.getTrailing? with
-  | some trailing => some trailing.stopPos
-  | none          => info.getTailPos? canonicalOnly
-
 end SourceInfo
 
 /--
@@ -3992,6 +3972,7 @@ position information.
 def getPos? (stx : Syntax) (canonicalOnly := false) : Option String.Pos :=
   stx.getHeadInfo.getPos? canonicalOnly
 
+
 /--
 Get the ending position of the syntax, if possible.
 If `canonicalOnly` is true, non-canonical `synthetic` nodes are treated as not carrying

src/Init/System/Uri.lean

@@ -29,13 +29,13 @@ def decodeUri (uri : String) : String := Id.run do
   let len := rawBytes.size
   let mut i := 0
   let percent := '%'.toNat.toUInt8
-  while h : i < len do
-    let c := rawBytes[i]
-    (decoded, i) := if h₁ : c == percent ∧ i + 1 < len then
-      let h1 := rawBytes[i + 1]
+  while i < len do
+    let c := rawBytes[i]!
+    (decoded, i) := if c == percent && i + 1 < len then
+      let h1 := rawBytes[i + 1]!
       if let some hd1 := hexDigitToUInt8? h1 then
-        if h₂ : i + 2 < len then
-          let h2 := rawBytes[i + 2]
+        if i + 2 < len then
+          let h2 := rawBytes[i + 2]!
           if let some hd2 := hexDigitToUInt8? h2 then
             -- decode the hex digits into a byte.
             (decoded.push (hd1 * 16 + hd2), i + 3)

src/Lean/Compiler/IR/EmitC.lean

@@ -271,9 +271,9 @@ def emitTag (x : VarId) (xType : IRType) : M Unit := do
     emit x
 
 def isIf (alts : Array Alt) : Option (Nat × FnBody × FnBody) :=
-  if h : alts.size ≠ 2 then none
-  else match alts[0] with
-    | Alt.ctor c b => some (c.cidx, b, alts[1].body)
+  if alts.size != 2 then none
+  else match alts[0]! with
+    | Alt.ctor c b => some (c.cidx, b, alts[1]!.body)
     | _            => none
 
 def emitInc (x : VarId) (n : Nat) (checkRef : Bool) : M Unit := do

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -1172,8 +1172,8 @@ def emitFnArgs (builder : LLVM.Builder llvmctx)
     (needsPackedArgs? : Bool)  (llvmfn : LLVM.Value llvmctx) (params : Array Param) : M llvmctx Unit := do
   if needsPackedArgs? then do
       let argsp ← LLVM.getParam llvmfn 0 -- lean_object **args
-      for h : i in [:params.size] do
-          let param := params[i]
+      for i in List.range params.size do
+          let param := params[i]!
           -- argsi := (args + i)
           let argsi ← LLVM.buildGEP2 builder (← LLVM.voidPtrType llvmctx) argsp #[← constIntUnsigned i] s!"packed_arg_{i}_slot"
           let llvmty ← toLLVMType param.ty
@@ -1182,16 +1182,15 @@ def emitFnArgs (builder : LLVM.Builder llvmctx)
           -- slot for arg[i] which is always void* ?
           let alloca ← buildPrologueAlloca builder llvmty s!"arg_{i}"
           LLVM.buildStore builder pv alloca
-          addVartoState param.x alloca llvmty
+          addVartoState params[i]!.x alloca llvmty
   else
       let n ← LLVM.countParams llvmfn
-      for i in [:n.toNat] do
-        let param := params[i]!
-        let llvmty ← toLLVMType param.ty
+      for i in (List.range n.toNat) do
+        let llvmty ← toLLVMType params[i]!.ty
         let alloca ← buildPrologueAlloca builder  llvmty s!"arg_{i}"
         let arg ← LLVM.getParam llvmfn (UInt64.ofNat i)
         let _ ← LLVM.buildStore builder arg alloca
-        addVartoState param.x alloca llvmty
+        addVartoState params[i]!.x alloca llvmty
 
 def emitDeclAux (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) (d : Decl) : M llvmctx Unit := do
   let env ← getEnv

src/Lean/Compiler/IR/ExpandResetReuse.lean

@@ -54,7 +54,7 @@ abbrev Mask := Array (Option VarId)
 partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (keep : Array FnBody) : Array FnBody × Mask :=
   let done (_ : Unit)        := (bs ++ keep.reverse, mask)
   let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop mask (keep.push b)
-  if h : bs.size < 2 then done ()
+  if bs.size < 2 then done ()
   else
     let b := bs.back!
     match b with
@@ -62,7 +62,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
     | .vdecl _ _ (.uproj _ _) _   => keepInstr b
     | .inc z n c p _ =>
       if n == 0 then done () else
-      let b' := bs[bs.size - 2]
+      let b' := bs[bs.size - 2]!
       match b' with
       | .vdecl w _ (.proj i x) _ =>
         if w == z && y == x then

src/Lean/Compiler/LCNF/Basic.lean

@@ -366,10 +366,10 @@ to be updated.
 @[implemented_by updateFunDeclCoreImp] opaque FunDeclCore.updateCore (decl: FunDecl) (type : Expr) (params : Array Param) (value : Code) : FunDecl
 
 def CasesCore.extractAlt! (cases : Cases) (ctorName : Name) : Alt × Cases :=
-  let found i := (cases.alts[i], { cases with alts := cases.alts.eraseIdx i })
-  if let some i := cases.alts.findFinIdx? fun | .alt ctorName' .. => ctorName == ctorName' | _ => false then
+  let found (i : Nat) := (cases.alts[i]!, { cases with alts := cases.alts.eraseIdx i })
+  if let some i := cases.alts.findIdx? fun | .alt ctorName' .. => ctorName == ctorName' | _ => false then
     found i
-  else if let some i := cases.alts.findFinIdx? fun | .default _ => true | _ => false then
+  else if let some i := cases.alts.findIdx? fun | .default _ => true | _ => false then
     found i
   else
     unreachable!

src/Lean/Compiler/LCNF/PassManager.lean

@@ -134,9 +134,9 @@ def withEachOccurrence (targetName : Name) (f : Nat → PassInstaller) : PassIns
 
 def installAfter (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0) : PassInstaller where
   install passes :=
-    if let some idx := passes.findFinIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
-      let passUnderTest := passes[idx]
-      return passes.insertIdx (idx + 1) (p passUnderTest)
+    if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
+      let passUnderTest := passes[idx]!
+      return passes.insertAt! (idx + 1) (p passUnderTest)
     else
       throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"
 
@@ -145,9 +145,9 @@ def installAfterEach (targetName : Name) (p : Pass → Pass) : PassInstaller :=
 
 def installBefore (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0): PassInstaller where
   install passes :=
-    if let some idx := passes.findFinIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
-      let passUnderTest := passes[idx]
-      return passes.insertIdx idx (p passUnderTest)
+    if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
+      let passUnderTest := passes[idx]!
+      return passes.insertAt! idx (p passUnderTest)
     else
       throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"
 

src/Lean/Compiler/LCNF/SpecInfo.lean

@@ -152,8 +152,8 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do
       let specArgs? := getSpecializationArgs? (← getEnv) decl.name
       let contains (i : Nat) : Bool := specArgs?.getD #[] |>.contains i
       let mut paramsInfo : Array SpecParamInfo := #[]
-      for h :i in [:decl.params.size] do
-        let param := decl.params[i]
+      for i in [:decl.params.size] do
+        let param := decl.params[i]!
         let info ←
           if contains i then
             pure .user
@@ -181,14 +181,14 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do
       declsInfo := declsInfo.push paramsInfo
   if declsInfo.any fun paramsInfo => paramsInfo.any (· matches .user | .fixedInst | .fixedHO) then
     let m := mkFixedParamsMap decls
-    for hi : i in [:decls.size] do
-      let decl := decls[i]
+    for i in [:decls.size] do
+      let decl := decls[i]!
       let mut paramsInfo := declsInfo[i]!
       let some mask := m.find? decl.name | unreachable!
       trace[Compiler.specialize.info] "{decl.name} {mask}"
       paramsInfo := paramsInfo.zipWith mask fun info fixed => if fixed || info matches .user then info else .other
       for j in [:paramsInfo.size] do
-        let mut info := paramsInfo[j]!
+        let mut info  := paramsInfo[j]!
         if info matches .fixedNeutral && !hasFwdDeps decl paramsInfo j then
           paramsInfo := paramsInfo.set! j .other
       if paramsInfo.any fun info => info matches .fixedInst | .fixedHO | .user then

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -499,8 +499,8 @@ where
       match app with
       | .fvar f =>
         let mut argsNew := #[]
-        for h :i in [arity : args.size] do
-          argsNew := argsNew.push (← visitAppArg args[i])
+        for i in [arity : args.size] do
+          argsNew := argsNew.push (← visitAppArg args[i]!)
         letValueToArg <| .fvar f argsNew
       | .erased | .type .. => return .erased
 

src/Lean/Compiler/Specialize.lean

@@ -26,14 +26,13 @@ private def elabSpecArgs (declName : Name) (args : Array Syntax) : MetaM (Array
       if let some idx := arg.isNatLit? then
         if idx == 0 then throwErrorAt arg "invalid specialization argument index, index must be greater than 0"
         let idx := idx - 1
-        if h : idx >= argNames.size then
+        if idx >= argNames.size then
           throwErrorAt arg "invalid argument index, `{declName}` has #{argNames.size} arguments"
-        else
-          if result.contains idx then throwErrorAt arg "invalid specialization argument index, `{argNames[idx]}` has already been specified as a specialization candidate"
-          result := result.push idx
+        if result.contains idx then throwErrorAt arg "invalid specialization argument index, `{argNames[idx]!}` has already been specified as a specialization candidate"
+        result := result.push idx
       else
         let argName := arg.getId
-        if let some idx := argNames.indexOf? argName then
+        if let some idx := argNames.getIdx? argName then
           if result.contains idx then throwErrorAt arg "invalid specialization argument name `{argName}`, it has already been specified as a specialization candidate"
           result := result.push idx
         else

src/Lean/Data/Lsp/Basic.lean

@@ -365,7 +365,6 @@ structure TextDocumentRegistrationOptions where
 
 inductive MarkupKind where
   | plaintext | markdown
-  deriving DecidableEq, Hashable
 
 instance : FromJson MarkupKind := ⟨fun
   | str "plaintext" => Except.ok MarkupKind.plaintext
@@ -379,7 +378,7 @@ instance : ToJson MarkupKind := ⟨fun
 structure MarkupContent where
   kind  : MarkupKind
   value : String
-  deriving ToJson, FromJson, DecidableEq, Hashable
+  deriving ToJson, FromJson
 
 /-- Reference to the progress of some in-flight piece of work.
 

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -25,7 +25,7 @@ inductive CompletionItemKind where
   | unit | value | enum | keyword | snippet
   | color | file | reference | folder | enumMember
   | constant | struct | event | operator | typeParameter
-  deriving Inhabited, DecidableEq, Repr, Hashable
+  deriving Inhabited, DecidableEq, Repr
 
 instance : ToJson CompletionItemKind where
   toJson a := toJson (a.toCtorIdx + 1)
@@ -39,11 +39,11 @@ structure InsertReplaceEdit where
   newText : String
   insert  : Range
   replace : Range
-  deriving FromJson, ToJson, BEq, Hashable
+  deriving FromJson, ToJson
 
 inductive CompletionItemTag where
   | deprecated
-  deriving Inhabited, DecidableEq, Repr, Hashable
+  deriving Inhabited, DecidableEq, Repr
 
 instance : ToJson CompletionItemTag where
   toJson t := toJson (t.toCtorIdx + 1)
@@ -73,7 +73,7 @@ structure CompletionItem where
   commitCharacters? : string[]
   command? : Command
   -/
-  deriving FromJson, ToJson, Inhabited, BEq, Hashable
+  deriving FromJson, ToJson, Inhabited
 
 structure CompletionList where
   isIncomplete : Bool

src/Lean/Data/PersistentHashMap.lean

@@ -233,10 +233,10 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β
   | n@(Node.collision keys vals heq), _, k =>
     match keys.indexOf? k with
     | some idx =>
-      let keys' := keys.eraseIdx idx
-      have keq := keys.size_eraseIdx idx _
-      let vals' := vals.eraseIdx (Eq.ndrec idx heq)
-      have veq := vals.size_eraseIdx (Eq.ndrec idx heq) _
+      let keys' := keys.feraseIdx idx
+      have keq := keys.size_feraseIdx idx
+      let vals' := vals.feraseIdx (Eq.ndrec idx heq)
+      have veq := vals.size_feraseIdx (Eq.ndrec idx heq)
       have : keys.size - 1 = vals.size - 1 := by rw [heq]
       Node.collision keys' vals' (keq.trans (this.trans veq.symm))
     | none     => n

src/Lean/Elab/App.lean

@@ -1347,7 +1347,7 @@ where
     let mut unusableNamedArgs := unusableNamedArgs
     for x in xs, bInfo in bInfos do
       let xDecl ← x.mvarId!.getDecl
-      if let some idx := remainingNamedArgs.findFinIdx? (·.name == xDecl.userName) then
+      if let some idx := remainingNamedArgs.findIdx? (·.name == xDecl.userName) then
         /- If there is named argument with name `xDecl.userName`, then it is accounted for and we can't make use of it. -/
         remainingNamedArgs := remainingNamedArgs.eraseIdx idx
       else
@@ -1355,9 +1355,9 @@ where
           /- We found a type of the form (baseName ...).
              First, we check if the current argument is an explicit one,
              and if the current explicit position "fits" at `args` (i.e., it must be ≤ arg.size) -/
-          if h : argIdx ≤ args.size ∧ bInfo.isExplicit then
+          if argIdx ≤ args.size && bInfo.isExplicit then
             /- We can insert `e` as an explicit argument -/
-            return (args.insertIdx argIdx (Arg.expr e), namedArgs)
+            return (args.insertAt! argIdx (Arg.expr e), namedArgs)
           else
             /- If we can't add `e` to `args`, we try to add it using a named argument, but this is only possible
                if there isn't an argument with the same name occurring before it. -/
@@ -1399,8 +1399,8 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
   let rec loop : Expr → List LVal → TermElabM Expr
   | f, []          => elabAppArgs f namedArgs args expectedType? explicit ellipsis
   | f, lval::lvals => do
-    if let LVal.fieldName (ref := ref) .. := lval then
-      addDotCompletionInfo ref f expectedType?
+    if let LVal.fieldName (fullRef := fullRef) .. := lval then
+      addDotCompletionInfo fullRef f expectedType?
     let hasArgs := !namedArgs.isEmpty || !args.isEmpty
     let (f, lvalRes) ← resolveLVal f lval hasArgs
     match lvalRes with
@@ -1650,14 +1650,6 @@ private def getSuccesses (candidates : Array (TermElabResult Expr)) : TermElabM
 -/
 private def mergeFailures (failures : Array (TermElabResult Expr)) : TermElabM α := do
   let exs := failures.map fun | .error ex _ => ex | _ => unreachable!
-  let trees := failures.map (fun | .error _ s => s.meta.core.infoState.trees | _ => unreachable!)
-    |>.filterMap (·[0]?)
-  -- Retain partial `InfoTree` subtrees in an `.ofChoiceInfo` node in case of multiple failures.
-  -- This ensures that the language server still has `Info` to work with when multiple overloaded
-  -- elaborators fail.
-  withInfoContext (mkInfo := pure <| .ofChoiceInfo { elaborator := .anonymous, stx := ← getRef }) do
-    for tree in trees do
-      pushInfoTree tree
   throwErrorWithNestedErrors "overloaded" exs
 
 private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array Arg) (ellipsis : Bool) (expectedType? : Option Expr) : TermElabM Expr := do

src/Lean/Elab/BuiltinCommand.lean

@@ -211,7 +211,7 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
         else
           `(bracketedBinderF| {$id $[: $ty?]?})
       for id in ids.reverse do
-        if let some idx := binderIds.findFinIdx? fun binderId => binderId.raw.isIdent && binderId.raw.getId == id.raw.getId then
+        if let some idx := binderIds.findIdx? fun binderId => binderId.raw.isIdent && binderId.raw.getId == id.raw.getId then
           binderIds := binderIds.eraseIdx idx
           modifiedVarDecls := true
           varDeclsNew := varDeclsNew.push (← mkBinder id explicit)

src/Lean/Elab/BuiltinTerm.lean

@@ -42,15 +42,16 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
 @[builtin_term_elab «completion»] def elabCompletion : TermElab := fun stx expectedType? => do
   /- `ident.` is ambiguous in Lean, we may try to be completing a declaration name or access a "field". -/
   if stx[0].isIdent then
-    -- Add both an `id` and a `dot` `CompletionInfo` and have the language server figure out which
-    -- one to use.
-    addCompletionInfo <| CompletionInfo.id stx stx[0].getId (danglingDot := true) (← getLCtx) expectedType?
+    /- If we can elaborate the identifier successfully, we assume it is a dot-completion. Otherwise, we treat it as
+       identifier completion with a dangling `.`.
+       Recall that the server falls back to identifier completion when dot-completion fails. -/
     let s ← saveState
     try
       let e ← elabTerm stx[0] none
       addDotCompletionInfo stx e expectedType?
     catch _ =>
       s.restore
+      addCompletionInfo <| CompletionInfo.id stx stx[0].getId (danglingDot := true) (← getLCtx) expectedType?
     throwErrorAt stx[1] "invalid field notation, identifier or numeral expected"
   else
     elabPipeCompletion stx expectedType?
@@ -327,7 +328,7 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
 @[builtin_term_elab withAnnotateTerm] def elabWithAnnotateTerm : TermElab := fun stx expectedType? => do
   match stx with
   | `(with_annotate_term $stx $e) =>
-    withTermInfoContext' .anonymous stx (expectedType? := expectedType?) (elabTerm e expectedType?)
+    withInfoContext' stx (elabTerm e expectedType?) (mkTermInfo .anonymous (expectedType? := expectedType?) stx)
   | _ => throwUnsupportedSyntax
 
 private unsafe def evalFilePathUnsafe (stx : Syntax) : TermElabM System.FilePath :=

src/Lean/Elab/Deriving/Util.lean

@@ -49,9 +49,9 @@ invoking ``mkInstImplicitBinders `BarClass foo #[`α, `n, `β]`` gives `` `([Bar
 def mkInstImplicitBinders (className : Name) (indVal : InductiveVal) (argNames : Array Name) : TermElabM (Array Syntax) :=
   forallBoundedTelescope indVal.type indVal.numParams fun xs _ => do
     let mut binders := #[]
-    for h : i in [:xs.size] do
+    for i in [:xs.size] do
       try
-        let x := xs[i]
+        let x := xs[i]!
         let c ← mkAppM className #[x]
         if (← isTypeCorrect c) then
           let argName := argNames[i]!
@@ -86,8 +86,8 @@ def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do
 
 def mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array Name) : TermElabM (Array (TSyntax ``Parser.Term.letDecl)) := do
   let mut letDecls := #[]
-  for h : i in [:ctx.typeInfos.size] do
-    let indVal       := ctx.typeInfos[i]
+  for i in [:ctx.typeInfos.size] do
+    let indVal       := ctx.typeInfos[i]!
     let auxFunName   := ctx.auxFunNames[i]!
     let currArgNames ← mkInductArgNames indVal
     let numParams    := indVal.numParams

src/Lean/Elab/Do.lean

@@ -796,10 +796,10 @@ Note that we are not restricting the macro power since the
 actions to be in the same universe.
 -/
 private def mkTuple (elems : Array Syntax) : MacroM Syntax := do
-  if elems.size = 0 then
+  if elems.size == 0 then
     mkUnit
-  else if h : elems.size = 1 then
-    return elems[0]
+  else if elems.size == 1 then
+    return elems[0]!
   else
     elems.extract 0 (elems.size - 1) |>.foldrM (init := elems.back!) fun elem tuple =>
       ``(MProd.mk $elem $tuple)
@@ -831,10 +831,10 @@ def isDoExpr? (doElem : Syntax) : Option Syntax :=
   We use this method when expanding the `for-in` notation.
 -/
 private def destructTuple (uvars : Array Var) (x : Syntax) (body : Syntax) : MacroM Syntax := do
-  if uvars.size = 0 then
+  if uvars.size == 0 then
     return body
-  else if h : uvars.size = 1 then
-    `(let $(uvars[0]):ident := $x; $body)
+  else if uvars.size == 1 then
+    `(let $(uvars[0]!):ident := $x; $body)
   else
     destruct uvars.toList x body
 where
@@ -1314,9 +1314,9 @@ private partial def expandLiftMethodAux (inQuot : Bool) (inBinder : Bool) : Synt
     else if liftMethodDelimiter k then
       return stx
     -- For `pure` if-then-else, we only lift `(<- ...)` occurring in the condition.
-    else if h : args.size >= 2 ∧ (k == ``termDepIfThenElse || k == ``termIfThenElse) then do
+    else if args.size >= 2 && (k == ``termDepIfThenElse || k == ``termIfThenElse) then do
       let inAntiquot := stx.isAntiquot && !stx.isEscapedAntiquot
-      let arg1 ← expandLiftMethodAux (inQuot && !inAntiquot || stx.isQuot) inBinder args[1]
+      let arg1 ← expandLiftMethodAux (inQuot && !inAntiquot || stx.isQuot) inBinder args[1]!
       let args := args.set! 1 arg1
       return Syntax.node i k args
     else if k == ``Parser.Term.liftMethod && !inQuot then withFreshMacroScope do
@@ -1518,7 +1518,7 @@ mutual
   -/
   partial def doForToCode (doFor : Syntax) (doElems : List Syntax) : M CodeBlock := do
     let doForDecls := doFor[1].getSepArgs
-    if h : doForDecls.size > 1 then
+    if doForDecls.size > 1 then
       /-
         Expand
         ```

src/Lean/Elab/Extra.lean

@@ -327,18 +327,15 @@ private def toExprCore (t : Tree) : TermElabM Expr := do
   | .term _ trees e =>
     modifyInfoState (fun s => { s with trees := s.trees ++ trees }); return e
   | .binop ref kind f lhs rhs =>
-    withRef ref <|
-      withTermInfoContext' .anonymous ref do
-        mkBinOp (kind == .lazy) f (← toExprCore lhs) (← toExprCore rhs)
+    withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) do
+      mkBinOp (kind == .lazy) f (← toExprCore lhs) (← toExprCore rhs)
   | .unop ref f arg =>
-    withRef ref <|
-      withTermInfoContext' .anonymous ref do
-        mkUnOp f (← toExprCore arg)
+    withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) do
+      mkUnOp f (← toExprCore arg)
   | .macroExpansion macroName stx stx' nested =>
-    withRef stx <|
-      withTermInfoContext' macroName stx <|
-        withMacroExpansion stx stx' <|
-          toExprCore nested
+    withRef stx <| withInfoContext' stx (mkInfo := mkTermInfo macroName stx) do
+      withMacroExpansion stx stx' do
+        toExprCore nested
 
 /--
   Auxiliary function to decide whether we should coerce `f`'s argument to `maxType` or not.

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
+    let commands := commands.push snap.data
     if let some next := snap.nextCmdSnap? then
       go initialSnap next.task commands
     else
@@ -115,9 +115,9 @@ where
       -- snapshots as they subsume any info trees reported incrementally by their children.
       let trees := commands.map (·.finishedSnap.get.infoTree?) |>.filterMap id |>.toPArray'
       return {
-        commandState := { snap.finishedSnap.get.cmdState with messages, infoState.trees := trees }
-        parserState := snap.parserState
-        cmdPos := snap.parserState.pos
+        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
       }
@@ -164,8 +164,8 @@ def runFrontend
     | return (← mkEmptyEnvironment, false)
 
   if let some out := trace.profiler.output.get? opts then
-    let traceStates := snaps.getAll.map (·.traces)
-    let profile ← Firefox.Profile.export mainModuleName.toString startTime traceStates opts
+    let traceState := cmdState.traceState
+    let profile ← Firefox.Profile.export mainModuleName.toString startTime traceState opts
     IO.FS.writeFile ⟨out⟩ <| Json.compress <| toJson profile
 
   let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)

src/Lean/Elab/Inductive.lean

@@ -173,15 +173,15 @@ private def checkUnsafe (rs : Array ElabHeaderResult) : TermElabM Unit := do
       throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes"
 
 private def InductiveView.checkLevelNames (views : Array InductiveView) : TermElabM Unit := do
-  if h : views.size > 1 then
-    let levelNames := views[0].levelNames
+  if views.size > 1 then
+    let levelNames := views[0]!.levelNames
     for view in views do
       unless view.levelNames == levelNames do
         throwErrorAt view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
 
 private def ElabHeaderResult.checkLevelNames (rs : Array ElabHeaderResult) : TermElabM Unit := do
-  if h : rs.size > 1 then
-    let levelNames := rs[0].levelNames
+  if rs.size > 1 then
+    let levelNames := rs[0]!.levelNames
     for r in rs do
       unless r.levelNames == levelNames do
         throwErrorAt r.view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
@@ -433,8 +433,8 @@ where
         let mut args := e.getAppArgs
         unless args.size ≥ params.size do
           throwError "unexpected inductive type occurrence{indentExpr e}"
-        for h : i in [:params.size] do
-          let param := params[i]
+        for i in [:params.size] do
+          let param := params[i]!
           let arg := args[i]!
           unless (← isDefEq param arg) do
             throwError "inductive datatype parameter mismatch{indentExpr arg}\nexpected{indentExpr param}"
@@ -694,8 +694,8 @@ private def collectLevelParamsInInductive (indTypes : List InductiveType) : Arra
 private def mkIndFVar2Const (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name) : ExprMap Expr := Id.run do
   let levelParams := levelNames.map mkLevelParam;
   let mut m : ExprMap Expr := {}
-  for h : i in [:views.size] do
-    let view    := views[i]
+  for i in [:views.size] do
+    let view    := views[i]!
     let indFVar := indFVars[i]!
     m := m.insert indFVar (mkConst view.declName levelParams)
   return m
@@ -856,9 +856,9 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
     withInductiveLocalDecls rs fun params indFVars => do
       trace[Elab.inductive] "indFVars: {indFVars}"
       let mut indTypesArray := #[]
-      for h : i in [:views.size] do
+      for i in [:views.size] do
         let indFVar := indFVars[i]!
-        Term.addLocalVarInfo views[i].declId indFVar
+        Term.addLocalVarInfo views[i]!.declId indFVar
         let r     := rs[i]!
         /- At this point, because of `withInductiveLocalDecls`, the only fvars that are in context are the ones related to the first inductive type.
            Because of this, we need to replace the fvars present in each inductive type's header of the mutual block with those of the first inductive.

src/Lean/Elab/InfoTree/Main.lean

@@ -139,16 +139,12 @@ def TermInfo.runMetaM (info : TermInfo) (ctx : ContextInfo) (x : MetaM α) : IO
 
 def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
   info.runMetaM ctx do
-    let ty : Format ←
-      try
-        Meta.ppExpr (← Meta.inferType info.expr)
-      catch _ =>
-        pure "<failed-to-infer-type>"
+    let ty : Format ← try
+      Meta.ppExpr (← Meta.inferType info.expr)
+    catch _ =>
+      pure "<failed-to-infer-type>"
     return f!"{← Meta.ppExpr info.expr} {if info.isBinder then "(isBinder := true) " else ""}: {ty} @ {formatElabInfo ctx info.toElabInfo}"
 
-def PartialTermInfo.format (ctx : ContextInfo) (info : PartialTermInfo) : Format :=
-  f!"Partial term @ {formatElabInfo ctx info.toElabInfo}"
-
 def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
   match info with
   | .dot i (expectedType? := expectedType?) .. => return f!"[.] {← i.format ctx} : {expectedType?}"
@@ -195,13 +191,9 @@ def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format
 def OmissionInfo.format (ctx : ContextInfo) (info : OmissionInfo) : IO Format := do
   return f!"Omission @ {← TermInfo.format ctx info.toTermInfo}\nReason: {info.reason}"
 
-def ChoiceInfo.format (ctx : ContextInfo) (info : ChoiceInfo) : Format :=
-  f!"Choice @ {formatElabInfo ctx info.toElabInfo}"
-
 def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofTacticInfo i         => i.format ctx
   | ofTermInfo i           => i.format ctx
-  | ofPartialTermInfo i    => pure <| i.format ctx
   | ofCommandInfo i        => i.format ctx
   | ofMacroExpansionInfo i => i.format ctx
   | ofOptionInfo i         => i.format ctx
@@ -212,12 +204,10 @@ def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofFVarAliasInfo i      => pure <| i.format
   | ofFieldRedeclInfo i    => pure <| i.format ctx
   | ofOmissionInfo i       => i.format ctx
-  | ofChoiceInfo i         => pure <| i.format ctx
 
 def Info.toElabInfo? : Info → Option ElabInfo
   | ofTacticInfo i         => some i.toElabInfo
   | ofTermInfo i           => some i.toElabInfo
-  | ofPartialTermInfo i    => some i.toElabInfo
   | ofCommandInfo i        => some i.toElabInfo
   | ofMacroExpansionInfo _ => none
   | ofOptionInfo _         => none
@@ -228,7 +218,6 @@ def Info.toElabInfo? : Info → Option ElabInfo
   | ofFVarAliasInfo _      => none
   | ofFieldRedeclInfo _    => none
   | ofOmissionInfo i       => some i.toElabInfo
-  | ofChoiceInfo i         => some i.toElabInfo
 
 /--
   Helper function for propagating the tactic metavariable context to its children nodes.
@@ -322,36 +311,24 @@ def realizeGlobalNameWithInfos (ref : Syntax) (id : Name) : CoreM (List (Name ×
       addConstInfo ref n
   return ns
 
-/--
-Adds a node containing the `InfoTree`s generated by `x` to the `InfoTree`s in `m`.
+/-- Use this to descend a node on the infotree that is being built.
 
-If `x` succeeds and `mkInfo` yields an `Info`, the `InfoTree`s of `x` become subtrees of a node
-containing the `Info` produced by `mkInfo`, which is then added to the `InfoTree`s in `m`.
-If `x` succeeds and `mkInfo` yields an `MVarId`, the `InfoTree`s of `x` are discarded and a `hole`
-node is added to the `InfoTree`s in `m`.
-If `x` fails, the `InfoTree`s of `x` become subtrees of a node containing the `Info` produced by
-`mkInfoOnError`, which is then added to the `InfoTree`s in `m`.
-
-The `InfoTree`s in `m` are reset before `x` is executed and restored with the addition of a new tree
-after `x` is executed.
--/
-def withInfoContext'
-    [MonadFinally m]
-    (x : m α)
-    (mkInfo : α → m (Sum Info MVarId))
-    (mkInfoOnError : m Info) :
-    m α := do
+It saves the current list of trees `t₀` and resets it and then runs `x >>= mkInfo`, producing either an `i : Info` or a hole id.
+Running `x >>= mkInfo` will modify the trees state and produce a new list of trees `t₁`.
+In the `i : Info` case, `t₁` become the children of a node `node i t₁` that is appended to `t₀`.
+ -/
+def withInfoContext' [MonadFinally m] (x : m α) (mkInfo : α → m (Sum Info MVarId)) : m α := do
   if (← getInfoState).enabled then
     let treesSaved ← getResetInfoTrees
     Prod.fst <$> MonadFinally.tryFinally' x fun a? => do
-      let info ← do
-        match a? with
-        | none => pure <| .inl <| ← mkInfoOnError
-        | some a => mkInfo a
-      modifyInfoTrees fun trees =>
-        match info with
-        | Sum.inl info   => treesSaved.push <| InfoTree.node info trees
-        | Sum.inr mvarId => treesSaved.push <| InfoTree.hole mvarId
+      match a? with
+      | none   => modifyInfoTrees fun _ => treesSaved
+      | some a =>
+        let info ← mkInfo a
+        modifyInfoTrees fun trees =>
+          match info with
+          | Sum.inl info   => treesSaved.push <| InfoTree.node info trees
+          | Sum.inr mvarId => treesSaved.push <| InfoTree.hole mvarId
   else
     x
 

src/Lean/Elab/InfoTree/Types.lean

@@ -70,18 +70,6 @@ structure TermInfo extends ElabInfo where
   isBinder : Bool := false
   deriving Inhabited
 
-/--
-Used instead of `TermInfo` when a term couldn't successfully be elaborated,
-and so there is no complete expression available.
-
-The main purpose of `PartialTermInfo` is to ensure that the sub-`InfoTree`s of a failed elaborator
-are retained so that they can still be used in the language server.
--/
-structure PartialTermInfo extends ElabInfo where
-  lctx : LocalContext -- The local context when the term was elaborated.
-  expectedType? : Option Expr
-  deriving Inhabited
-
 structure CommandInfo extends ElabInfo where
   deriving Inhabited
 
@@ -91,7 +79,7 @@ inductive CompletionInfo where
   | dot (termInfo : TermInfo) (expectedType? : Option Expr)
   | id (stx : Syntax) (id : Name) (danglingDot : Bool) (lctx : LocalContext) (expectedType? : Option Expr)
   | dotId (stx : Syntax) (id : Name) (lctx : LocalContext) (expectedType? : Option Expr)
-  | fieldId (stx : Syntax) (id : Option Name) (lctx : LocalContext) (structName : Name)
+  | fieldId (stx : Syntax) (id : Name) (lctx : LocalContext) (structName : Name)
   | namespaceId (stx : Syntax)
   | option (stx : Syntax)
   | endSection (stx : Syntax) (scopeNames : List String)
@@ -177,18 +165,10 @@ regular delaboration settings.
 structure OmissionInfo extends TermInfo where
   reason : String
 
-/--
-Indicates that all overloaded elaborators failed. The subtrees of a `ChoiceInfo` node are the
-partial `InfoTree`s of those failed elaborators. Retaining these partial `InfoTree`s helps
-the language server provide interactivity even when all overloaded elaborators failed.
--/
-structure ChoiceInfo extends ElabInfo where
-
 /-- Header information for a node in `InfoTree`. -/
 inductive Info where
   | ofTacticInfo (i : TacticInfo)
   | ofTermInfo (i : TermInfo)
-  | ofPartialTermInfo (i : PartialTermInfo)
   | ofCommandInfo (i : CommandInfo)
   | ofMacroExpansionInfo (i : MacroExpansionInfo)
   | ofOptionInfo (i : OptionInfo)
@@ -199,7 +179,6 @@ inductive Info where
   | ofFVarAliasInfo (i : FVarAliasInfo)
   | ofFieldRedeclInfo (i : FieldRedeclInfo)
   | ofOmissionInfo (i : OmissionInfo)
-  | ofChoiceInfo (i : ChoiceInfo)
   deriving Inhabited
 
 /-- The InfoTree is a structure that is generated during elaboration and used

src/Lean/Elab/LetRec.lean

@@ -87,15 +87,12 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
   view.decls.mapM fun view => do
     forallBoundedTelescope view.type view.binderIds.size fun xs type => do
       -- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location.
-      for h : i in [0:view.binderIds.size] do
-        addLocalVarInfo view.binderIds[i] xs[i]!
+      for i in [0:view.binderIds.size] do
+        addLocalVarInfo view.binderIds[i]! xs[i]!
       withDeclName view.declName do
-        withInfoContext' view.valStx
-          (mkInfo := (pure <| .inl <| mkBodyInfo view.valStx ·))
-          (mkInfoOnError := (pure <| mkBodyInfo view.valStx none))
-          do
-             let value ← elabTermEnsuringType view.valStx type
-             mkLambdaFVars xs value
+        withInfoContext' view.valStx (mkInfo := (pure <| .inl <| mkBodyInfo view.valStx ·)) do
+          let value ← elabTermEnsuringType view.valStx type
+          mkLambdaFVars xs value
 
 private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array Expr) (values : Array Expr) : TermElabM Unit := do
   let letRecsToLiftCurr := (← get).letRecsToLift

src/Lean/Elab/Match.lean

@@ -282,8 +282,8 @@ where
         let dArg := dArgs[i]!
         unless (← isDefEq tArg dArg) do
           return i :: (← goType tArg dArg)
-      for h : i in [info.numParams : tArgs.size] do
-        let tArg := tArgs[i]
+      for i in [info.numParams : tArgs.size] do
+        let tArg := tArgs[i]!
         let dArg := dArgs[i]!
         unless (← isDefEq tArg dArg) do
           return i :: (← goIndex tArg dArg)
@@ -644,7 +644,7 @@ where
       if inaccessible? p |>.isSome then
         return mkMData k (← withReader (fun _ => true) (go b))
       else if let some (stx, p) := patternWithRef? p then
-        Elab.withInfoContext' (go p) (mkInfoOnError := mkPartialTermInfo .anonymous stx) fun p => do
+        Elab.withInfoContext' (go p) fun p => do
           /- If `p` is a free variable and we are not inside of an "inaccessible" pattern, this `p` is a binder. -/
           mkTermInfo Name.anonymous stx p (isBinder := p.isFVar && !(← read))
       else

src/Lean/Elab/MutualDef.lean

@@ -283,7 +283,7 @@ private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) (
   loop 0 #[]
 
 private def expandWhereStructInst : Macro
-  | whereStx@`(Parser.Command.whereStructInst|where%$whereTk $[$decls:letDecl];* $[$whereDecls?:whereDecls]?) => do
+  | `(Parser.Command.whereStructInst|where $[$decls:letDecl];* $[$whereDecls?:whereDecls]?) => do
     let letIdDecls ← decls.mapM fun stx => match stx with
       | `(letDecl|$_decl:letPatDecl) => Macro.throwErrorAt stx "patterns are not allowed here"
       | `(letDecl|$decl:letEqnsDecl) => expandLetEqnsDecl decl (useExplicit := false)
@@ -300,30 +300,7 @@ private def expandWhereStructInst : Macro
         `(structInstField|$id:ident := $val)
       | stx@`(letIdDecl|_ $_* $[: $_]? := $_) => Macro.throwErrorAt stx "'_' is not allowed here"
       | _ => Macro.throwUnsupported
-
-    let startOfStructureTkInfo : SourceInfo :=
-      match whereTk.getPos? with
-      | some pos => .synthetic pos ⟨pos.byteIdx + 1⟩ true
-      | none => .none
-    -- Position the closing `}` at the end of the trailing whitespace of `where $[$_:letDecl];*`.
-    -- We need an accurate range of the generated structure instance in the generated `TermInfo`
-    -- so that we can determine the expected type in structure field completion.
-    let structureStxTailInfo :=
-      whereStx[1].getTailInfo?
-      <|> whereStx[0].getTailInfo?
-    let endOfStructureTkInfo : SourceInfo :=
-      match structureStxTailInfo with
-      | some (SourceInfo.original _ _ trailing _) =>
-        let tokenPos := trailing.str.prev trailing.stopPos
-        let tokenEndPos := trailing.stopPos
-        .synthetic tokenPos tokenEndPos true
-      | _ => .none
-
     let body ← `(structInst| { $structInstFields,* })
-    let body := body.raw.setInfo <|
-      match startOfStructureTkInfo.getPos?, endOfStructureTkInfo.getTailPos? with
-      | some startPos, some endPos => .synthetic startPos endPos true
-      | _, _ => .none
     match whereDecls? with
     | some whereDecls => expandWhereDecls whereDecls body
     | none => return body
@@ -440,15 +417,12 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
           -- Store instantiated body in info tree for the benefit of the unused variables linter
           -- and other metaprograms that may want to inspect it without paying for the instantiation
           -- again
-          withInfoContext' valStx
-            (mkInfo := (pure <| .inl <| mkBodyInfo valStx ·))
-            (mkInfoOnError := (pure <| mkBodyInfo valStx none))
-            do
-              -- synthesize mvars here to force the top-level tactic block (if any) to run
-              let val ← elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
-              -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
-              -- leads to more section variables being included than necessary
-              instantiateMVarsProfiling val
+          withInfoContext' valStx (mkInfo := (pure <| .inl <| mkBodyInfo valStx ·)) do
+            -- synthesize mvars here to force the top-level tactic block (if any) to run
+            let val ← elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
+            -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
+            -- leads to more section variables being included than necessary
+            instantiateMVarsProfiling val
         let val ← mkLambdaFVars xs val
         if linter.unusedSectionVars.get (← getOptions) && !header.type.hasSorry && !val.hasSorry then
           let unusedVars ← vars.filterMapM fun var => do

src/Lean/Elab/Open.lean

@@ -49,12 +49,12 @@ private def resolveNameUsingNamespacesCore (nss : List Name) (idStx : Syntax) :
       exs := exs.push ex
   if exs.size == nss.length then
     withRef idStx do
-      if h : exs.size = 1 then
-        throw exs[0]
+      if exs.size == 1 then
+        throw exs[0]!
       else
         throwErrorWithNestedErrors "failed to open" exs
-  if h : result.size = 1 then
-    return result[0]
+  if result.size == 1 then
+    return result[0]!
   else
     withRef idStx do throwError "ambiguous identifier '{idStx.getId}', possible interpretations: {result.map mkConst}"
 

src/Lean/Elab/PatternVar.lean

@@ -332,9 +332,9 @@ where
     else
       let accessible := isNextArgAccessible ctx
       let (d, ctx)   := getNextParam ctx
-      match ctx.namedArgs.findFinIdx? fun namedArg => namedArg.name == d.1 with
+      match ctx.namedArgs.findIdx? fun namedArg => namedArg.name == d.1 with
       | some idx =>
-        let arg := ctx.namedArgs[idx]
+        let arg := ctx.namedArgs[idx]!
         let ctx := { ctx with namedArgs := ctx.namedArgs.eraseIdx idx }
         let ctx ← pushNewArg accessible ctx arg.val
         processCtorAppContext ctx

src/Lean/Elab/PreDefinition/Basic.lean

@@ -244,8 +244,8 @@ def checkCodomainsLevel (preDefs : Array PreDefinition) : MetaM Unit := do
     lambdaTelescope preDef.value fun xs _ => return xs.size
   forallBoundedTelescope preDefs[0]!.type arities[0]!  fun _ type₀ => do
     let u₀ ← getLevel type₀
-    for h : i in [1:preDefs.size] do
-      forallBoundedTelescope preDefs[i].type arities[i]! fun _ typeᵢ =>
+    for i in [1:preDefs.size] do
+      forallBoundedTelescope preDefs[i]!.type arities[i]! fun _ typeᵢ =>
       unless ← isLevelDefEq u₀ (← getLevel typeᵢ) do
         withOptions (fun o => pp.sanitizeNames.set o false) do
           throwError m!"invalid mutual definition, result types must be in the same universe " ++

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

@@ -292,9 +292,9 @@ def mkBrecOnApp (positions : Positions) (fnIdx : Nat) (brecOnConst : Nat → Exp
     let packedFTypes ← inferArgumentTypesN positions.size brecOn
     let packedFArgs ← positions.mapMwith PProdN.mkLambdas packedFTypes FArgs
     let brecOn := mkAppN brecOn packedFArgs
-    let some (size, idx) := positions.findSome? fun pos => (pos.size, ·) <$> pos.indexOf? fnIdx
+    let some poss := positions.find? (·.contains fnIdx)
       | throwError "mkBrecOnApp: Could not find {fnIdx} in {positions}"
-    let brecOn ← PProdN.proj size idx brecOn
+    let brecOn ← PProdN.proj poss.size (poss.getIdx? fnIdx).get! brecOn
     mkLambdaFVars ys (mkAppN brecOn otherArgs)
 
 end Lean.Elab.Structural

src/Lean/Elab/PreDefinition/TerminationArgument.lean

@@ -53,10 +53,10 @@ def TerminationArgument.elab (funName : Name) (type : Expr) (arity extraParams :
     (hint : TerminationBy) : TermElabM TerminationArgument := withDeclName funName do
   assert! extraParams ≤ arity
 
-  if h : hint.vars.size > extraParams then
+  if hint.vars.size > extraParams then
     let mut msg := m!"{parameters hint.vars.size} bound in `termination_by`, but the body of " ++
       m!"{funName} only binds {parameters extraParams}."
-    if let `($ident:ident) := hint.vars[0] then
+    if let `($ident:ident) := hint.vars[0]! then
       if ident.getId.isSuffixOf funName then
           msg := msg ++ m!" (Since Lean v4.6.0, the `termination_by` clause no longer " ++
             "expects the function name here.)"

src/Lean/Elab/PreDefinition/TerminationHint.lean

@@ -90,10 +90,10 @@ lambda of `value`, and throws appropriate errors.
 -/
 def TerminationBy.checkVars (funName : Name) (extraParams : Nat) (tb : TerminationBy) : MetaM Unit := do
   unless tb.synthetic do
-    if h : tb.vars.size > extraParams then
+    if tb.vars.size > extraParams then
       let mut msg := m!"{parameters tb.vars.size} bound in `termination_by`, but the body of " ++
         m!"{funName} only binds {parameters extraParams}."
-      if let `($ident:ident) := tb.vars[0] then
+      if let `($ident:ident) := tb.vars[0]! then
         if ident.getId.isSuffixOf funName then
             msg := msg ++ m!" (Since Lean v4.6.0, the `termination_by` clause no longer " ++
               "expects the function name here.)"

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

@@ -21,8 +21,8 @@ open Meta
 private partial def addNonRecPreDefs (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition)  : TermElabM Unit := do
   let us := preDefNonRec.levelParams.map mkLevelParam
   let all := preDefs.toList.map (·.declName)
-  for h : fidx in [:preDefs.size] do
-    let preDef := preDefs[fidx]
+  for fidx in [:preDefs.size] do
+    let preDef := preDefs[fidx]!
     let value ← forallBoundedTelescope preDef.type (some fixedPrefixSize) fun xs _ => do
       let value := mkAppN (mkConst preDefNonRec.declName us) xs
       let value ← argsPacker.curryProj value fidx

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

@@ -40,7 +40,7 @@ private partial def post (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames
     return TransformStep.done e
   let declName := f.constName!
   let us       := f.constLevels!
-  if let some fidx := funNames.indexOf? declName then
+  if let some fidx := funNames.getIdx? declName then
     let arity := fixedPrefix + argsPacker.varNamess[fidx]!.size
     let e' ← withAppN arity e fun args => do
       let fixedArgs := args[:fixedPrefix]

src/Lean/Elab/Print.lean

@@ -22,7 +22,7 @@ private def levelParamsToMessageData (levelParams : List Name) : MessageData :=
       m := m ++ ", " ++ toMessageData u
     return m ++ "}"
 
-private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) (sig : Bool := true) : CommandElabM MessageData := do
+private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM MessageData := do
   let m : MessageData :=
     match (← getReducibilityStatus id) with
     | ReducibilityStatus.irreducible => "@[irreducible] "
@@ -38,13 +38,11 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type
   let (m, id) := match privateToUserName? id with
     | some id => (m ++ "private ", id)
     | none    => (m, id)
-  if sig then
-    return m!"{m}{kind} {id}{levelParamsToMessageData levelParams} : {type}"
-  else
-    return m!"{m}{kind}"
+  let m := m ++ kind ++ " " ++ id ++ levelParamsToMessageData levelParams ++ " : " ++ type
+  pure m
 
-private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) (sig : Bool := true) : CommandElabM MessageData :=
-  mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe) (sig := sig)
+private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData :=
+  mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe)
 
 private def printDefLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (value : Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do
   let m ← mkHeader kind id levelParams type safety
@@ -67,63 +65,32 @@ private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat)
     m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
   logInfo m
 
-/--
-Computes the origin of a field. Returns its projection function at the origin.
-Multiple parents could be the origin of a field, but we say the first parent that provides it is the one that determines the origin.
--/
-private partial def getFieldOrigin (structName field : Name) : MetaM Name := do
-  let env ← getEnv
-  for parent in getStructureParentInfo env structName do
-    if (findField? env parent.structName field).isSome then
-      return ← getFieldOrigin parent.structName field
-  let some fi := getFieldInfo? env structName field
-    | throwError "no such field {field} in {structName}"
-  return fi.projFn
-
 open Meta in
 private def printStructure (id : Name) (levelParams : List Name) (numParams : Nat) (type : Expr)
-    (isUnsafe : Bool) : CommandElabM Unit := do
-  let env ← getEnv
-  let kind := if isClass env id then "class" else "structure"
-  let header ← mkHeader' kind id levelParams type isUnsafe (sig := false)
-  liftTermElabM <| forallTelescope (← getConstInfo id).type fun params _ =>
-    let s := Expr.const id (levelParams.map .param)
-    withLocalDeclD `self (mkAppN s params) fun self => do
-      let mut m : MessageData := header
-      -- Signature
-      m := m ++ " " ++ .ofFormatWithInfosM do
-        let (stx, infos) ← PrettyPrinter.delabCore s (delab := PrettyPrinter.Delaborator.delabConstWithSignature)
-        pure ⟨← PrettyPrinter.ppTerm ⟨stx⟩, infos⟩
-      m := m ++ Format.line ++ m!"number of parameters: {numParams}"
-      -- Parents
-      let parents := getStructureParentInfo env id
-      unless parents.isEmpty do
-        m := m ++ Format.line ++ "parents:"
-        for parent in parents do
-          let ptype ← inferType (mkApp (mkAppN (.const parent.projFn (levelParams.map .param)) params) self)
-          m := m ++ indentD m!"{.ofConstName parent.projFn (fullNames := true)} : {ptype}"
-      -- Fields
-      let fields := getStructureFieldsFlattened env id (includeSubobjectFields := false)
-      if fields.isEmpty then
-        m := m ++ Format.line ++ "fields: (none)"
-      else
-        m := m ++ Format.line ++ "fields:"
+    (ctor : Name) (fields : Array Name) (isUnsafe : Bool) (isClass : Bool) : CommandElabM Unit := do
+  let kind := if isClass then "class" else "structure"
+  let mut m ← mkHeader' kind id levelParams type isUnsafe
+  m := m ++ Format.line ++ "number of parameters: " ++ toString numParams
+  m := m ++ Format.line ++ "constructor:"
+  let cinfo ← getConstInfo ctor
+  m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
+  m := m ++ Format.line ++ "fields:" ++ (← doFields)
+  logInfo m
+where
+  doFields := liftTermElabM do
+    forallTelescope (← getConstInfo id).type fun params _ =>
+      withLocalDeclD `self (mkAppN (Expr.const id (levelParams.map .param)) params) fun self => do
+        let params := params.push self
+        let mut m : MessageData := ""
         for field in fields do
-          let some source := findField? env id field | panic! "missing structure field info"
-          let proj ← getFieldOrigin source field
-          let modifier := if isPrivateName proj then "private " else ""
-          let ftype ← inferType (← mkProjection self field)
-          m := m ++ indentD (m!"{modifier}{.ofConstName proj (fullNames := true)} : {ftype}")
-      -- Constructor
-      let cinfo := getStructureCtor (← getEnv) id
-      let ctorModifier := if isPrivateName cinfo.name then "private " else ""
-      m := m ++ Format.line ++ "constructor:" ++ indentD (ctorModifier ++ .signature cinfo.name)
-      -- Resolution order
-      let resOrder ← getStructureResolutionOrder id
-      if resOrder.size > 1 then
-        m := m ++ Format.line ++ "resolution order:"
-          ++ indentD (MessageData.joinSep (resOrder.map (.ofConstName · (fullNames := true))).toList ", ")
-      logInfo m
+          match getProjFnForField? (← getEnv) id field with
+          | some proj =>
+            let field : Format := if isPrivateName proj then "private " ++ toString field else toString field
+            let cinfo ← getConstInfo proj
+            let ftype ← instantiateForall cinfo.type params
+            m := m ++ Format.line ++ field ++ " : " ++ ftype
+          | none => panic! "missing structure field info"
+        addMessageContext m
 
 private def printIdCore (id : Name) : CommandElabM Unit := do
   let env ← getEnv
@@ -136,10 +103,11 @@ private def printIdCore (id : Name) : CommandElabM Unit := do
   | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
   | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
   | ConstantInfo.inductInfo { levelParams := us, numParams, type := t, ctors, isUnsafe := u, .. } =>
-    if isStructure env id then
-      printStructure id us numParams t u
-    else
-      printInduct id us numParams t ctors u
+    match getStructureInfo? env id with
+    | some { fieldNames, .. } =>
+      let [ctor] := ctors | panic! "structures have only one constructor"
+      printStructure id us numParams t ctor fieldNames u (isClass env id)
+    | none => printInduct id us numParams t ctors u
   | none => throwUnknownId id
 
 private def printId (id : Syntax) : CommandElabM Unit := do

src/Lean/Elab/Quotation.lean

@@ -58,7 +58,7 @@ partial def mkTuple : Array Syntax → TermElabM Syntax
   | #[]  => `(Unit.unit)
   | #[e] => return e
   | es   => do
-    let stx ← mkTuple (es.eraseIdxIfInBounds 0)
+    let stx ← mkTuple (es.eraseIdx 0)
     `(Prod.mk $(es[0]!) $stx)
 
 def resolveSectionVariable (sectionVars : NameMap Name) (id : Name) : List (Name × List String) :=

src/Lean/Elab/StructInst.lean

@@ -186,7 +186,7 @@ def structInstArrayRef := leading_parser "[" >> termParser >>"]"
 ```
 -/
 private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
-  let s? ← stx[2][0].getSepArgs.foldlM (init := none) fun s? arg => do
+  let s? ← stx[2].getSepArgs.foldlM (init := none) fun s? arg => do
     /- arg is of the form `structInstFieldAbbrev <|> structInstField` -/
     if arg.getKind == ``Lean.Parser.Term.structInstField then
       /- Remark: the syntax for `structInstField` is
@@ -245,7 +245,7 @@ private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSource
     let valField  := modifyOp.setArg 0 <| mkNode ``Parser.Term.structInstLVal #[valFirst, valRest]
     let valSource := mkSourcesWithSyntax #[s]
     let val       := stx.setArg 1 valSource
-    let val       := val.setArg 2 <| mkNode ``Parser.Term.structInstFields #[mkNullNode #[valField]]
+    let val       := val.setArg 2 <| mkNullNode #[valField]
     trace[Elab.struct.modifyOp] "{stx}\nval: {val}"
     cont val
 
@@ -440,7 +440,7 @@ private def mkStructView (stx : Syntax) (structName : Name) (sources : SourcesVi
   /- Recall that `stx` is of the form
      ```
      leading_parser "{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
-                 >> structInstFields (sepByIndent (structInstFieldAbbrev <|> structInstField) ...)
+                 >> sepByIndent (structInstFieldAbbrev <|> structInstField) ...
                  >> optional ".."
                  >> optional (" : " >> termParser)
                  >> " }"
@@ -448,7 +448,7 @@ private def mkStructView (stx : Syntax) (structName : Name) (sources : SourcesVi
 
      This method assumes that `structInstFieldAbbrev` had already been expanded.
   -/
-  let fields ← stx[2][0].getSepArgs.toList.mapM fun fieldStx => do
+  let fields ← stx[2].getSepArgs.toList.mapM fun fieldStx => do
     let val      := fieldStx[2]
     let first    ← toFieldLHS fieldStx[0][0]
     let rest     ← fieldStx[0][1].getArgs.toList.mapM toFieldLHS
@@ -602,9 +602,7 @@ mutual
             let valStx := s.ref -- construct substructure syntax using s.ref as template
             let valStx := valStx.setArg 4 mkNullNode -- erase optional expected type
             let args   := substructFields.toArray.map (·.toSyntax)
-            let fieldsStx := mkNode ``Parser.Term.structInstFields
-              #[mkNullNode <| mkSepArray args (mkAtom ",")]
-            let valStx := valStx.setArg 2 fieldsStx
+            let valStx := valStx.setArg 2 (mkNullNode <| mkSepArray args (mkAtom ","))
             let valStx ← updateSource valStx
             return { field with lhs := [field.lhs.head!], val := FieldVal.term valStx }
   /--

src/Lean/Elab/Syntax.lean

@@ -19,12 +19,12 @@ def expandOptPrecedence (stx : Syntax) : MacroM (Option Nat) :=
     return some (← evalPrec stx[0][1])
 
 private def mkParserSeq (ds : Array (Term × Nat)) : TermElabM (Term × Nat) := do
-  if h₀ : ds.size = 0 then
+  if ds.size == 0 then
     throwUnsupportedSyntax
-  else if h₁ : ds.size = 1 then
-    pure ds[0]
+  else if ds.size == 1 then
+    pure ds[0]!
   else
-    let mut (r, stackSum) := ds[0]
+    let mut (r, stackSum) := ds[0]!
     for (d, stackSz) in ds[1:ds.size] do
       r ← `(ParserDescr.binary `andthen $r $d)
       stackSum := stackSum + stackSz
@@ -142,7 +142,7 @@ where
     let args := stx.getArgs
     if (← checkLeftRec stx[0]) then
       if args.size == 1 then throwErrorAt stx "invalid atomic left recursive syntax"
-      let args := args.eraseIdxIfInBounds 0
+      let args := args.eraseIdx 0
       let args ← args.mapM fun arg => withNestedParser do process arg
       mkParserSeq args
     else

src/Lean/Elab/SyntheticMVars.lean

@@ -149,8 +149,8 @@ where
         -- Succeeded. Collect new TC problems
         trace[Elab.defaultInstance] "isDefEq worked {mkMVar mvarId} : {← inferType (mkMVar mvarId)} =?= {candidate} : {← inferType candidate}"
         let mut pending := []
-        for h : i in [:bis.size] do
-          if bis[i] == BinderInfo.instImplicit then
+        for i in [:bis.size] do
+          if bis[i]! == BinderInfo.instImplicit then
             pending := mvars[i]!.mvarId! :: pending
         synthesizePending pending
       else

src/Lean/Elab/Tactic/Basic.lean

@@ -218,7 +218,7 @@ where
                     let old ← snap.old?
                     -- If the kind is equal, we can assume the old version was a macro as well
                     guard <| old.stx.isOfKind stx.getKind
-                    let state ← old.val.get.finished.get.state?
+                    let state ← old.val.get.data.finished.get.state?
                     guard <| state.term.meta.core.nextMacroScope == nextMacroScope
                     -- check absence of traces; see Note [Incremental Macros]
                     guard <| state.term.meta.core.traceState.traces.size == 0
@@ -226,10 +226,9 @@ where
                     return old.val.get
                   Language.withAlwaysResolvedPromise fun promise => do
                     -- Store new unfolding in the snapshot tree
-                    snap.new.resolve {
+                    snap.new.resolve <| .mk {
                       stx := stx'
                       diagnostics := .empty
-                      inner? := none
                       finished := .pure {
                         diagnostics := .empty
                         state? := (← Tactic.saveState)
@@ -241,7 +240,7 @@ where
                       new := promise
                       old? := do
                         let old ← old?
-                        return ⟨old.stx, (← old.next.get? 0)⟩
+                        return ⟨old.data.stx, (← old.data.next.get? 0)⟩
                     } }) do
                       evalTactic stx'
                   return

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -60,7 +60,7 @@ where
     if let some snap := (← readThe Term.Context).tacSnap? then
       if let some old := snap.old? then
         let oldParsed := old.val.get
-        oldInner? := oldParsed.inner? |>.map (⟨oldParsed.stx, ·⟩)
+        oldInner? := oldParsed.data.inner? |>.map (⟨oldParsed.data.stx, ·⟩)
     -- compare `stx[0]` for `finished`/`next` reuse, focus on remainder of script
     Term.withNarrowedTacticReuse (stx := stx) (fun stx => (stx[0], mkNullNode stx.getArgs[1:])) fun stxs => do
       let some snap := (← readThe Term.Context).tacSnap?
@@ -70,10 +70,10 @@ where
       if let some old := snap.old? then
         -- `tac` must be unchanged given the narrow above; let's reuse `finished`'s state!
         let oldParsed := old.val.get
-        if let some state := oldParsed.finished.get.state? then
+        if let some state := oldParsed.data.finished.get.state? then
           reusableResult? := some ((), state)
           -- only allow `next` reuse in this case
-          oldNext? := oldParsed.next.get? 0 |>.map (⟨old.stx, ·⟩)
+          oldNext? := oldParsed.data.next.get? 0 |>.map (⟨old.stx, ·⟩)
 
       -- For `tac`'s snapshot task range, disregard synthetic info as otherwise
       -- `SnapshotTree.findInfoTreeAtPos` might choose the wrong snapshot: for example, when
@@ -89,7 +89,7 @@ where
       withAlwaysResolvedPromise fun next => do
         withAlwaysResolvedPromise fun finished => do
           withAlwaysResolvedPromise fun inner => do
-            snap.new.resolve {
+            snap.new.resolve <| .mk {
               desc := tac.getKind.toString
               diagnostics := .empty
               stx := tac

src/Lean/Elab/Tactic/Config.lean

@@ -114,13 +114,6 @@ private def elabConfig (recover : Bool) (structName : Name) (items : Array Confi
     let e ← Term.withSynthesize <| Term.elabTermEnsuringType stx (mkConst structName)
     instantiateMVars e
 
-section
--- We automatically disable the following option for `macro`s but the subsequent `def` both contains
--- a quotation and is called only by `macro`s, so we disable the option for it manually. Note that
--- we can't use `in` as it is parsed as a single command and so the option would not influence the
--- parser.
-set_option internal.parseQuotWithCurrentStage false
-
 private def mkConfigElaborator
     (doc? : Option (TSyntax ``Parser.Command.docComment)) (elabName type monadName : Ident)
     (adapt recover : Term) : MacroM (TSyntax `command) := do
@@ -155,8 +148,6 @@ private def mkConfigElaborator
             throwError msg
       go)
 
-end
-
 /-!
 `declare_config_elab elabName TypeName` declares a function `elabName : Syntax → TacticM TypeName`
 that elaborates a tactic configuration.

src/Lean/Elab/Tactic/Induction.lean

@@ -282,11 +282,10 @@ where
         -- them, eventually put each of them back in `Context.tacSnap?` in `applyAltStx`
         withAlwaysResolvedPromise fun finished => do
           withAlwaysResolvedPromises altStxs.size fun altPromises => do
-            tacSnap.new.resolve {
+            tacSnap.new.resolve <| .mk {
               -- save all relevant syntax here for comparison with next document version
               stx := mkNullNode altStxs
               diagnostics := .empty
-              inner? := none
               finished := { range? := none, task := finished.result }
               next := altStxs.zipWith altPromises fun stx prom =>
                 { range? := stx.getRange?, task := prom.result }
@@ -299,7 +298,7 @@ where
                 let old := old.val.get
                 -- use old version of `mkNullNode altsSyntax` as guard, will be compared with new
                 -- version and picked apart in `applyAltStx`
-                return ⟨old.stx, (← old.next[i]?)⟩
+                return ⟨old.data.stx, (← old.data.next[i]?)⟩
               new := prom
             }
             finished.resolve { diagnostics := .empty, state? := (← saveState) }
@@ -341,9 +340,9 @@ where
     for h : altStxIdx in [0:altStxs.size] do
       let altStx := altStxs[altStxIdx]
       let altName := getAltName altStx
-      if let some i := alts.findFinIdx? (·.1 == altName) then
+      if let some i := alts.findIdx? (·.1 == altName) then
         -- cover named alternative
-        applyAltStx tacSnaps altStxIdx altStx alts[i]
+        applyAltStx tacSnaps altStxIdx altStx alts[i]!
         alts := alts.eraseIdx i
       else if !alts.isEmpty && isWildcard altStx then
         -- cover all alternatives

src/Lean/Elab/Term.lean

@@ -230,7 +230,7 @@ instance : ToSnapshotTree TacticFinishedSnapshot where
   toSnapshotTree s := ⟨s.toSnapshot, #[]⟩
 
 /-- Snapshot just before execution of a tactic. -/
-structure TacticParsedSnapshot extends Language.Snapshot where
+structure TacticParsedSnapshotData (TacticParsedSnapshot : Type) extends Language.Snapshot where
   /-- Syntax tree of the tactic, stored and compared for incremental reuse. -/
   stx      : Syntax
   /-- Task for nested incrementality, if enabled for tactic. -/
@@ -240,9 +240,16 @@ structure TacticParsedSnapshot extends Language.Snapshot where
   /-- Tasks for subsequent, potentially parallel, tactic steps. -/
   next     : Array (SnapshotTask TacticParsedSnapshot) := #[]
 deriving Inhabited
+
+/-- State after execution of a single synchronous tactic step. -/
+inductive TacticParsedSnapshot where
+  | mk (data : TacticParsedSnapshotData TacticParsedSnapshot)
+deriving Inhabited
+abbrev TacticParsedSnapshot.data : TacticParsedSnapshot → TacticParsedSnapshotData TacticParsedSnapshot
+  | .mk data => data
 partial instance : ToSnapshotTree TacticParsedSnapshot where
   toSnapshotTree := go where
-    go := fun s => ⟨s.toSnapshot,
+    go := fun ⟨s⟩ => ⟨s.toSnapshot,
       s.inner?.toArray.map (·.map (sync := true) go) ++
       #[s.finished.map (sync := true) toSnapshotTree] ++
       s.next.map (·.map (sync := true) go)⟩
@@ -1291,20 +1298,13 @@ def isTacticOrPostponedHole? (e : Expr) : TermElabM (Option MVarId) := do
     | _                                  => return none
   | _ => pure none
 
-def mkTermInfo (elaborator : Name) (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none)
-    (lctx? : Option LocalContext := none) (isBinder := false) :
-    TermElabM (Sum Info MVarId) := do
+def mkTermInfo (elaborator : Name) (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (isBinder := false) : TermElabM (Sum Info MVarId) := do
   match (← isTacticOrPostponedHole? e) with
   | some mvarId => return Sum.inr mvarId
   | none =>
     let e := removeSaveInfoAnnotation e
     return Sum.inl <| Info.ofTermInfo { elaborator, lctx := lctx?.getD (← getLCtx), expr := e, stx, expectedType?, isBinder }
 
-def mkPartialTermInfo (elaborator : Name) (stx : Syntax) (expectedType? : Option Expr := none)
-    (lctx? : Option LocalContext := none) :
-    TermElabM Info := do
-  return Info.ofPartialTermInfo { elaborator, lctx := lctx?.getD (← getLCtx), stx, expectedType? }
-
 /--
 Pushes a new leaf node to the info tree associating the expression `e` to the syntax `stx`.
 As a result, when the user hovers over `stx` they will see the type of `e`, and if `e`
@@ -1326,54 +1326,41 @@ def addTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none)
   if (← read).inPattern && !force then
     return mkPatternWithRef e stx
   else
-    discard <| withInfoContext'
-      (pure ())
-      (fun _ => mkTermInfo elaborator stx e expectedType? lctx? isBinder)
-      (mkPartialTermInfo elaborator stx expectedType? lctx?)
+    withInfoContext' (pure ()) (fun _ => mkTermInfo elaborator stx e expectedType? lctx? isBinder) |> discard
     return e
 
 def addTermInfo' (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (elaborator := Name.anonymous) (isBinder := false) : TermElabM Unit :=
   discard <| addTermInfo stx e expectedType? lctx? elaborator isBinder
 
-def withInfoContext' (stx : Syntax) (x : TermElabM Expr)
-    (mkInfo : Expr → TermElabM (Sum Info MVarId)) (mkInfoOnError : TermElabM Info) :
-    TermElabM Expr := do
+def withInfoContext' (stx : Syntax) (x : TermElabM Expr) (mkInfo : Expr → TermElabM (Sum Info MVarId)) : TermElabM Expr := do
   if (← read).inPattern then
     let e ← x
     return mkPatternWithRef e stx
   else
-    Elab.withInfoContext' x mkInfo mkInfoOnError
+    Elab.withInfoContext' x mkInfo
 
 /-- Info node capturing `def/let rec` bodies, used by the unused variables linter. -/
 structure BodyInfo where
-  /-- The body as a fully elaborated term. `none` if the body failed to elaborate. -/
-  value? : Option Expr
+  /-- The body as a fully elaborated term. -/
+  value : Expr
 deriving TypeName
 
 /-- Creates an `Info.ofCustomInfo` node backed by a `BodyInfo`. -/
-def mkBodyInfo (stx : Syntax) (value? : Option Expr) : Info :=
-  .ofCustomInfo { stx, value := .mk { value? : BodyInfo } }
+def mkBodyInfo (stx : Syntax) (value : Expr) : Info :=
+  .ofCustomInfo { stx, value := .mk { value : BodyInfo } }
 
 /-- Extracts a `BodyInfo` custom info. -/
 def getBodyInfo? : Info → Option BodyInfo
   | .ofCustomInfo { value, .. } => value.get? BodyInfo
   | _ => none
 
-def withTermInfoContext' (elaborator : Name) (stx : Syntax) (x : TermElabM Expr)
-    (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none)
-    (isBinder : Bool := false) :
-    TermElabM Expr :=
-  withInfoContext' stx x
-    (mkTermInfo elaborator stx (expectedType? := expectedType?) (lctx? := lctx?) (isBinder := isBinder))
-    (mkPartialTermInfo elaborator stx (expectedType? := expectedType?) (lctx? := lctx?))
-
 /--
 Postpone the elaboration of `stx`, return a metavariable that acts as a placeholder, and
 ensures the info tree is updated and a hole id is introduced.
 When `stx` is elaborated, new info nodes are created and attached to the new hole id in the info tree.
 -/
 def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
-  withTermInfoContext' .anonymous stx (expectedType? := expectedType?) do
+  withInfoContext' stx (mkInfo := mkTermInfo .anonymous (expectedType? := expectedType?) stx) do
     postponeElabTermCore stx expectedType?
 
 /--
@@ -1385,7 +1372,7 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? :
   | (elabFn::elabFns) =>
     try
       -- record elaborator in info tree, but only when not backtracking to other elaborators (outer `try`)
-      withTermInfoContext' elabFn.declName stx (expectedType? := expectedType?)
+      withInfoContext' stx (mkInfo := mkTermInfo elabFn.declName (expectedType? := expectedType?) stx)
         (try
           elabFn.value stx expectedType?
         catch ex => match ex with
@@ -1768,7 +1755,7 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
     let result ← match (← liftMacroM (expandMacroImpl? env stx)) with
     | some (decl, stxNew?) =>
       let stxNew ← liftMacroM <| liftExcept stxNew?
-      withTermInfoContext' decl stx (expectedType? := expectedType?) <|
+      withInfoContext' stx (mkInfo := mkTermInfo decl (expectedType? := expectedType?) stx) <|
         withMacroExpansion stx stxNew <|
           withRef stxNew <|
             elabTermAux expectedType? catchExPostpone implicitLambda stxNew

src/Lean/Environment.lean

@@ -317,8 +317,8 @@ partial def ensureExtensionsArraySize (exts : Array EnvExtensionState) : IO (Arr
 where
   loop (i : Nat) (exts : Array EnvExtensionState) : IO (Array EnvExtensionState) := do
     let envExtensions ← envExtensionsRef.get
-    if h : i < envExtensions.size then
-      let s ← envExtensions[i].mkInitial
+    if i < envExtensions.size then
+      let s ← envExtensions[i]!.mkInitial
       let exts := exts.push s
       loop (i + 1) exts
     else
@@ -726,6 +726,7 @@ def mkExtNameMap (startingAt : Nat) : IO (Std.HashMap Name Nat) := do
   let descrs ← persistentEnvExtensionsRef.get
   let mut result := {}
   for h : i in [startingAt : descrs.size] do
+    have : i < descrs.size := h.upper
     let descr := descrs[i]
     result := result.insert descr.name i
   return result
@@ -739,6 +740,7 @@ private def setImportedEntries (env : Environment) (mods : Array ModuleData) (st
   /- For each module `mod`, and `mod.entries`, if the extension name is one of the extensions after `startingAt`, set `entries` -/
   let extNameIdx ← mkExtNameMap startingAt
   for h : modIdx in [:mods.size] do
+    have : modIdx < mods.size := h.upper
     let mod := mods[modIdx]
     for (extName, entries) in mod.entries do
       if let some entryIdx := extNameIdx[extName]? then
@@ -858,7 +860,7 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
   let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.empty (capacity := numConsts)
   let mut constantMap : Std.HashMap Name ConstantInfo := Std.HashMap.empty (capacity := numConsts)
   for h : modIdx in [0:s.moduleData.size] do
-    let mod := s.moduleData[modIdx]
+    let mod := s.moduleData[modIdx]'h.upper
     for cname in mod.constNames, cinfo in mod.constants do
       match constantMap.getThenInsertIfNew? cname cinfo with
       | (cinfoPrev?, constantMap') =>

src/Lean/Language/Basic.lean

@@ -56,11 +56,6 @@ structure Snapshot where
   /-- General elaboration metadata produced by this step. -/
   infoTree? : Option Elab.InfoTree := none
   /--
-  Trace data produced by this step. Currently used only by `trace.profiler.output`, otherwise we
-  depend on the elaborator adding traces to `diagnostics` eventually.
-  -/
-  traces : TraceState := {}
-  /--
   Whether it should be indicated to the user that a fatal error (which should be part of
   `diagnostics`) occurred that prevents processing of the remainder of the file.
   -/

src/Lean/Language/Lean.lean

@@ -348,7 +348,7 @@ where
         if let some (some processed) ← old.processedResult.get? then
           -- ...and the edit location is after the next command (see note [Incremental Parsing])...
           if let some nextCom ← processed.firstCmdSnap.get? then
-            if (← isBeforeEditPos nextCom.parserState.pos) then
+            if (← isBeforeEditPos nextCom.data.parserState.pos) then
               -- ...go immediately to next snapshot
               return (← unchanged old old.stx oldSuccess.parserState)
 
@@ -470,20 +470,20 @@ where
       -- from `old`
       if let some oldNext := old.nextCmdSnap? then do
         let newProm ← IO.Promise.new
-        let _ ← old.finishedSnap.bindIO (sync := true) fun oldFinished =>
+        let _ ← old.data.finishedSnap.bindIO (sync := true) fun oldFinished =>
           -- also wait on old command parse snapshot as parsing is cheap and may allow for
           -- elaboration reuse
           oldNext.bindIO (sync := true) fun oldNext => do
             parseCmd oldNext newParserState oldFinished.cmdState newProm sync ctx
             return .pure ()
-        prom.resolve <| { old with nextCmdSnap? := some { range? := none, task := newProm.result } }
+        prom.resolve <| .mk (data := old.data) (nextCmdSnap? := some { range? := none, task := newProm.result })
       else prom.resolve old  -- terminal command, we're done!
 
     -- fast path, do not even start new task for this snapshot
     if let some old := old? then
       if let some nextCom ← old.nextCmdSnap?.bindM (·.get?) then
-        if (← isBeforeEditPos nextCom.parserState.pos) then
-          return (← unchanged old old.parserState)
+        if (← isBeforeEditPos nextCom.data.parserState.pos) then
+          return (← unchanged old old.data.parserState)
 
     let beginPos := parserState.pos
     let scope := cmdState.scopes.head!
@@ -500,7 +500,7 @@ where
       -- NOTE: as `parserState.pos` includes trailing whitespace, this forces reprocessing even if
       -- only that whitespace changes, which is wasteful but still necessary because it may
       -- influence the range of error messages such as from a trailing `exact`
-      if stx.eqWithInfo old.stx then
+      if stx.eqWithInfo old.data.stx then
         -- Here we must make sure to pass the *new* parser state; see NOTE in `unchanged`
         return (← unchanged old parserState)
       -- on first change, make sure to cancel old invocation
@@ -515,12 +515,11 @@ where
       -- this is a bit ugly as we don't want to adjust our API with `Option`s just for cancellation
       -- (as no-one should look at this result in that case) but anything containing `Environment`
       -- is not `Inhabited`
-      prom.resolve <| {
+      prom.resolve <| .mk (nextCmdSnap? := none) {
         diagnostics := .empty, stx := .missing, parserState
         elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
         finishedSnap := .pure { diagnostics := .empty, cmdState }
         tacticCache := (← IO.mkRef {})
-        nextCmdSnap? := none
       }
       return
 
@@ -538,30 +537,29 @@ where
       -- irrelevant in this case.
       let endRange? := stx.getTailPos?.map fun pos => ⟨pos, pos⟩
       let finishedSnap := { range? := endRange?, task := finishedPromise.result }
-      let tacticCache ← old?.map (·.tacticCache) |>.getDM (IO.mkRef {})
+      let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
 
       let minimalSnapshots := internal.cmdlineSnapshots.get cmdState.scopes.head!.opts
       let next? ← if Parser.isTerminalCommand stx then pure none
         -- for now, wait on "command finished" snapshot before parsing next command
         else some <$> IO.Promise.new
-      let nextCmdSnap? := next?.map
-        ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })
       let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog
-      if minimalSnapshots && !Parser.isTerminalCommand stx then
-        prom.resolve {
-          diagnostics, finishedSnap, tacticCache, nextCmdSnap?
-          stx := .missing
-          parserState := {}
-          elabSnap := { range? := stx.getRange?, task := elabPromise.result }
-        }
-      else
-        prom.resolve {
-          diagnostics, stx, parserState, tacticCache, nextCmdSnap?
-          elabSnap := { range? := stx.getRange?, task := elabPromise.result }
-          finishedSnap
-        }
+      let data := if minimalSnapshots && !Parser.isTerminalCommand stx then {
+        diagnostics
+        stx := .missing
+        parserState := {}
+        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+        finishedSnap
+        tacticCache
+      } else {
+        diagnostics, stx, parserState, tacticCache
+        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+        finishedSnap
+      }
+      prom.resolve <| .mk (nextCmdSnap? := next?.map
+        ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })) data
       let cmdState ← doElab stx cmdState beginPos
-        { old? := old?.map fun old => ⟨old.stx, old.elabSnap⟩, new := elabPromise }
+        { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
         finishedPromise tacticCache ctx
       if let some next := next? then
         -- We're definitely off the fast-forwarding path now
@@ -573,7 +571,7 @@ where
       LeanProcessingM Command.State := do
     let ctx ← read
     let scope := cmdState.scopes.head!
-    let cmdStateRef ← IO.mkRef { cmdState with messages := .empty, traceState := {} }
+    let cmdStateRef ← IO.mkRef { cmdState with messages := .empty }
     /-
     The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel`
     has exclusive access to the cache, we create a fresh reference here. Before this change, the
@@ -615,7 +613,6 @@ where
     finishedPromise.resolve {
       diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages)
       infoTree? := infoTree
-      traces := cmdState.traceState
       cmdState := if cmdline then {
         env := Runtime.markPersistent cmdState.env
         maxRecDepth := 0
@@ -647,6 +644,6 @@ where goCmd snap :=
   if let some next := snap.nextCmdSnap? then
     goCmd next.get
   else
-    snap.finishedSnap.get.cmdState
+    snap.data.finishedSnap.get.cmdState
 
 end Lean

src/Lean/Language/Lean/Types.lean

@@ -34,7 +34,7 @@ instance : ToSnapshotTree CommandFinishedSnapshot where
   toSnapshotTree s := ⟨s.toSnapshot, #[]⟩
 
 /-- State after a command has been parsed. -/
-structure CommandParsedSnapshot extends Snapshot where
+structure CommandParsedSnapshotData extends Snapshot where
   /-- Syntax tree of the command. -/
   stx : Syntax
   /-- Resulting parser state. -/
@@ -48,14 +48,27 @@ structure CommandParsedSnapshot extends Snapshot where
   finishedSnap : SnapshotTask CommandFinishedSnapshot
   /-- Cache for `save`; to be replaced with incrementality. -/
   tacticCache : IO.Ref Tactic.Cache
-  /-- Next command, unless this is a terminal command. -/
-  nextCmdSnap? : Option (SnapshotTask CommandParsedSnapshot)
 deriving Nonempty
+
+/-- State after a command has been parsed. -/
+-- workaround for lack of recursive structures
+inductive CommandParsedSnapshot where
+  /-- Creates a command parsed snapshot. -/
+  | mk (data : CommandParsedSnapshotData)
+    (nextCmdSnap? : Option (SnapshotTask CommandParsedSnapshot))
+deriving Nonempty
+/-- The snapshot data. -/
+abbrev CommandParsedSnapshot.data : CommandParsedSnapshot → CommandParsedSnapshotData
+  | mk data _ => data
+/-- Next command, unless this is a terminal command. -/
+abbrev CommandParsedSnapshot.nextCmdSnap? : CommandParsedSnapshot →
+    Option (SnapshotTask CommandParsedSnapshot)
+  | mk _ next? => next?
 partial instance : ToSnapshotTree CommandParsedSnapshot where
   toSnapshotTree := go where
-    go s := ⟨s.toSnapshot,
-      #[s.elabSnap.map (sync := true) toSnapshotTree,
-        s.finishedSnap.map (sync := true) toSnapshotTree] |>
+    go s := ⟨s.data.toSnapshot,
+      #[s.data.elabSnap.map (sync := true) toSnapshotTree,
+        s.data.finishedSnap.map (sync := true) toSnapshotTree] |>
         pushOpt (s.nextCmdSnap?.map (·.map (sync := true) go))⟩
 
 /-- State after successful importing. -/

src/Lean/Level.lean

@@ -599,20 +599,17 @@ def geq (u v : Level) : Bool :=
 where
   go (u v : Level) : Bool :=
     u == v ||
-    let k := fun () =>
-      match v with
-      | imax v₁ v₂ => go u v₁ && go u v₂
-      | _          =>
-        let v' := v.getLevelOffset
-        (u.getLevelOffset == v' || v'.isZero)
-        && u.getOffset ≥ v.getOffset
     match u, v with
-    | _,          zero      => true
-    | u,          max v₁ v₂ => go u v₁ && go u v₂
-    | max u₁ u₂,  v         => go u₁ v || go u₂ v || k ()
-    | imax _  u₂, v         => go u₂ v
-    | succ u,     succ v    => go u v
-    | _,          _         => k ()
+    | _,          zero       => true
+    | u,          max v₁ v₂  => go u v₁ && go u v₂
+    | max u₁ u₂,  v          => go u₁ v || go u₂ v
+    | u,          imax v₁ v₂ => go u v₁ && go u v₂
+    | imax _  u₂, v          => go u₂ v
+    | succ u,     succ v     => go u v
+    | _, _ =>
+      let v' := v.getLevelOffset
+      (u.getLevelOffset == v' || v'.isZero)
+      && u.getOffset ≥ v.getOffset
   termination_by (u, v)
 
 end Level

src/Lean/Linter/UnusedVariables.lean

@@ -393,17 +393,16 @@ where
         | .ofCustomInfo ti =>
           if !linter.unusedVariables.analyzeTactics.get ci.options then
             if let some bodyInfo := ti.value.get? Elab.Term.BodyInfo then
-              if let some value := bodyInfo.value? then
-                -- the body is the only `Expr` we will analyze in this case
-                -- NOTE: we include it even if no tactics are present as at least for parameters we want
-                -- to lint only truly unused binders
-                let (e, _) := instantiateMVarsCore ci.mctx value
-                modify fun s => { s with
-                  assignments := s.assignments.push (.insert {} ⟨.anonymous⟩ e) }
-                let tacticsPresent := children.any (·.findInfo? (· matches .ofTacticInfo ..) |>.isSome)
-                withReader (· || tacticsPresent) do
-                  go children.toArray ci
-                return false
+              -- the body is the only `Expr` we will analyze in this case
+              -- NOTE: we include it even if no tactics are present as at least for parameters we want
+              -- to lint only truly unused binders
+              let (e, _) := instantiateMVarsCore ci.mctx bodyInfo.value
+              modify fun s => { s with
+                assignments := s.assignments.push (.insert {} ⟨.anonymous⟩ e) }
+              let tacticsPresent := children.any (·.findInfo? (· matches .ofTacticInfo ..) |>.isSome)
+              withReader (· || tacticsPresent) do
+                go children.toArray ci
+              return false
         | .ofTermInfo ti =>
           if ignored then return true
           match ti.expr with

src/Lean/Message.lean

@@ -244,8 +244,8 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
       | panic! s!"MessageData.ofLazy: expected MessageData in Dynamic, got {dyn.typeName}"
     formatAux nCtx ctx? msg
 
-protected def format (msgData : MessageData) (ctx? : Option MessageDataContext := none) : IO Format :=
-  formatAux { currNamespace := Name.anonymous, openDecls := [] } ctx? msgData
+protected def format (msgData : MessageData) : IO Format :=
+  formatAux { currNamespace := Name.anonymous, openDecls := [] } none msgData
 
 protected def toString (msgData : MessageData) : IO String := do
   return toString (← msgData.format)

src/Lean/Meta/CongrTheorems.lean

@@ -122,8 +122,8 @@ def mkHCongr (f : Expr) : MetaM CongrTheorem := do
 private def fixKindsForDependencies (info : FunInfo) (kinds : Array CongrArgKind) : Array CongrArgKind := Id.run do
   let mut kinds := kinds
   for i in [:info.paramInfo.size] do
-    for hj : j in [i+1:info.paramInfo.size] do
-      if info.paramInfo[j].backDeps.contains i then
+    for j in [i+1:info.paramInfo.size] do
+      if info.paramInfo[j]!.backDeps.contains i then
         if kinds[j]! matches CongrArgKind.eq || kinds[j]! matches CongrArgKind.fixed then
           -- We must fix `i` because there is a `j` that depends on `i` and `j` is not cast-fixed.
           kinds := kinds.set! i CongrArgKind.fixed

src/Lean/Meta/ExprDefEq.lean

@@ -255,8 +255,8 @@ private def isDefEqArgsFirstPass
     (paramInfo : Array ParamInfo) (args₁ args₂ : Array Expr) : MetaM DefEqArgsFirstPassResult := do
   let mut postponedImplicit := #[]
   let mut postponedHO := #[]
-  for h : i in [:paramInfo.size] do
-    let info := paramInfo[i]
+  for i in [:paramInfo.size] do
+    let info := paramInfo[i]!
     let a₁ := args₁[i]!
     let a₂ := args₂[i]!
     if info.dependsOnHigherOrderOutParam || info.higherOrderOutParam then
@@ -939,6 +939,29 @@ def check (hasCtxLocals : Bool) (mctx : MetavarContext) (lctx : LocalContext) (m
 
 end CheckAssignmentQuick
 
+/--
+Auxiliary function used at `typeOccursCheckImp`.
+Given `type`, it tries to eliminate "dependencies". For example, suppose we are trying to
+perform the assignment `?m := f (?n a b)` where
+```
+?n : let k := g ?m; A -> h k ?m -> C
+```
+If we just perform occurs check `?m` at the type of `?n`, we get a failure, but
+we claim these occurrences are ok because the type `?n a b : C`.
+In the example above, `typeOccursCheckImp` invokes this function with `n := 2`.
+Note that we avoid using `whnf` and `inferType` at `typeOccursCheckImp` to minimize the
+performance impact of this extra check.
+
+See test `typeOccursCheckIssue.lean` for an example where this refinement is needed.
+The test is derived from a Mathlib file.
+-/
+private partial def skipAtMostNumBinders (type : Expr) (n : Nat) : Expr :=
+  match type, n with
+  | .forallE _ _ b _, n+1 => skipAtMostNumBinders b n
+  | .mdata _ b,       n   => skipAtMostNumBinders b n
+  | .letE _ _ v b _,  n   => skipAtMostNumBinders (b.instantiate1 v) n
+  | type,             _   => type
+
 /-- `typeOccursCheck` implementation using unsafe (i.e., pointer equality) features. -/
 private unsafe def typeOccursCheckImp (mctx : MetavarContext) (mvarId : MVarId) (v : Expr) : Bool :=
   if v.hasExprMVar then
@@ -959,11 +982,19 @@ where
     -- this function assumes all assigned metavariables have already been
     -- instantiated.
     go.run' mctx
-  visitMVar (mvarId' : MVarId) : Bool :=
+  visitMVar (mvarId' : MVarId) (numArgs : Nat := 0) : Bool :=
     if let some mvarDecl := mctx.findDecl? mvarId' then
-      occursCheck mvarDecl.type
+      occursCheck (skipAtMostNumBinders mvarDecl.type numArgs)
     else
       false
+  visitApp (e : Expr) : StateM (PtrSet Expr) Bool :=
+    e.withApp fun f args => do
+      unless (← args.allM visit) do
+        return false
+      if f.isMVar then
+        return visitMVar f.mvarId! args.size
+      else
+        visit f
   visit (e : Expr) : StateM (PtrSet Expr) Bool := do
     if !e.hasExprMVar then
       return true
@@ -972,7 +1003,7 @@ where
     else match e with
       | .mdata _ b       => visit b
       | .proj _ _ s      => visit s
-      | .app f a         => visit f <&&> visit a
+      | .app ..          => visitApp e
       | .lam _ d b _     => visit d <&&> visit b
       | .forallE _ d b _ => visit d <&&> visit b
       | .letE _ t v b _  => visit t <&&> visit v <&&> visit b
@@ -1356,21 +1387,15 @@ private abbrev unfold (e : Expr) (failK : MetaM α) (successK : Expr → MetaM
 /-- Auxiliary method for isDefEqDelta -/
 private def unfoldBothDefEq (fn : Name) (t s : Expr) : MetaM LBool := do
   match t, s with
-  | .const _ ls₁, .const _ ls₂ =>
-    match (← isListLevelDefEq ls₁ ls₂) with
-    | .true => return .true
-    | _ =>
-    unfold t (pure .undef) fun t =>
-    unfold s (pure .undef) fun s =>
-      isDefEqLeftRight fn t s
-  | .app _ _,     .app _ _     =>
+  | Expr.const _ ls₁, Expr.const _ ls₂ => isListLevelDefEq ls₁ ls₂
+  | Expr.app _ _,     Expr.app _ _     =>
     if (← tryHeuristic t s) then
-      return .true
+      pure LBool.true
     else
       unfold t
-       (unfold s (pure .undef) fun s => isDefEqRight fn t s)
+       (unfold s (pure LBool.undef) (fun s => isDefEqRight fn t s))
        (fun t => unfold s (isDefEqLeft fn t s) (fun s => isDefEqLeftRight fn t s))
-  | _, _ => return .false
+  | _, _ => pure LBool.false
 
 private def sameHeadSymbol (t s : Expr) : Bool :=
   match t.getAppFn, s.getAppFn with
@@ -1649,12 +1674,11 @@ private partial def isDefEqQuick (t s : Expr) : MetaM LBool :=
   -- | Expr.mdata _ t _,    s                   => isDefEqQuick t s
   -- | t,                   Expr.mdata _ s _    => isDefEqQuick t s
   | .fvar fvarId₁, .fvar fvarId₂ => do
-    if fvarId₁ == fvarId₂ then
-      return .true
-    else if (← fvarId₁.isLetVar <||> fvarId₂.isLetVar) then
-      return .undef
+    if (← fvarId₁.isLetVar <||> fvarId₂.isLetVar) then
+      return LBool.undef
+    else if fvarId₁ == fvarId₂ then
+      return LBool.true
     else
-      -- If `t` and `s` are not proofs or let-variables, we still return `.undef` and let other rules (e.g., unit-like) kick in.
       isDefEqProofIrrel t s
   | t, s =>
     isDefEqQuickOther t s

src/Lean/Meta/ForEachExpr.lean

@@ -93,8 +93,8 @@ def setMVarUserNamesAt (e : Expr) (isTarget : Array Expr) : MetaM (Array MVarId)
   forEachExpr (← instantiateMVars e) fun e => do
     if e.isApp then
       let args := e.getAppArgs
-      for h : i in [:args.size] do
-        let arg := args[i]
+      for i in [:args.size] do
+        let arg := args[i]!
         if arg.isMVar && isTarget.contains arg then
           let mvarId := arg.mvarId!
           if (← mvarId.getDecl).userName.isAnonymous then

src/Lean/Meta/IndPredBelow.lean

@@ -83,7 +83,7 @@ where
       forallTelescopeReducing t fun xs s => do
         let motiveType ← instantiateForall motive xs[:numParams]
         withLocalDecl motiveName BinderInfo.implicit motiveType fun motive => do
-          mkForallFVars (xs.insertIdxIfInBounds numParams motive) s)
+          mkForallFVars (xs.insertAt! numParams motive) s)
 
   motiveType (indVal : InductiveVal) : MetaM Expr :=
     forallTelescopeReducing indVal.type fun xs _ => do

src/Lean/Meta/Match/MatchEqs.lean

@@ -129,9 +129,9 @@ where
           let typeNew := b.instantiate1 y
           if let some (_, lhs, rhs) ← matchEq? d then
             if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then
-               let some j  := ys.indexOf? lhs | unreachable!
+               let some j  := ys.getIdx? lhs | unreachable!
                let ys      := ys.eraseIdx j
-               let some k  := args.indexOf? lhs | unreachable!
+               let some k  := args.getIdx? lhs | unreachable!
                let mask    := mask.set! k false
                let args    := args.map fun arg => if arg == lhs then rhs else arg
                let arg     ← mkEqRefl rhs
@@ -557,8 +557,8 @@ where
         let mut minorBodyNew := minor
         -- We have to extend the mapping to make sure `convertTemplate` can "fix" occurrences of the refined minor premises
         let mut m ← read
-        for h : i in [:isAlt.size] do
-          if isAlt[i] then
+        for i in [:isAlt.size] do
+          if isAlt[i]! then
             -- `convertTemplate` will correct occurrences of the alternative
             let alt := args[6+i]! -- Recall that `Eq.ndrec` has 6 arguments
             let some (_, numParams, argMask) := m.find? alt.fvarId! | unreachable!

src/Lean/Meta/RecursorInfo.lean

@@ -107,7 +107,7 @@ private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs :
     if motiveArgs.isEmpty then
       throwError "invalid user defined recursor, '{declName}' does not support dependent elimination, and position of the major premise was not specified (solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)"
     let major := motiveArgs.back!
-    match xs.indexOf? major with
+    match xs.getIdx? major with
     | some majorPos => pure (major, majorPos, true)
     | none          => throwError "ill-formed recursor '{declName}'"
 

src/Lean/Meta/Tactic/Clear.lean

@@ -27,7 +27,7 @@ def _root_.Lean.MVarId.clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId
       throwTacticEx `clear mvarId m!"target depends on '{mkFVar fvarId}'"
     let lctx := lctx.erase fvarId
     let localInsts ← getLocalInstances
-    let localInsts := match localInsts.findFinIdx? fun localInst => localInst.fvar.fvarId! == fvarId with
+    let localInsts := match localInsts.findIdx? fun localInst => localInst.fvar.fvarId! == fvarId with
       | none => localInsts
       | some idx => localInsts.eraseIdx idx
     let newMVar ← mkFreshExprMVarAt lctx localInsts mvarDecl.type MetavarKind.syntheticOpaque tag

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -148,13 +148,13 @@ def mkCustomEliminator (elimName : Name) (induction : Bool) : MetaM CustomElimin
   let info ← getConstInfo elimName
   forallTelescopeReducing info.type fun xs _ => do
     let mut typeNames := #[]
-    for hi : i in [:elimInfo.targetsPos.size] do
-      let targetPos := elimInfo.targetsPos[i]
+    for i in [:elimInfo.targetsPos.size] do
+      let targetPos := elimInfo.targetsPos[i]!
       let x := xs[targetPos]!
       /- Return true if there is another target that depends on `x`. -/
       let isImplicitTarget : MetaM Bool := do
-        for hj : j in [i+1:elimInfo.targetsPos.size] do
-          let y := xs[elimInfo.targetsPos[j]]!
+        for j in [i+1:elimInfo.targetsPos.size] do
+          let y := xs[elimInfo.targetsPos[j]!]!
           let yType ← inferType y
           if (← dependsOn yType x.fvarId!) then
             return true

src/Lean/Meta/Tactic/Simp/SimpAll.lean

@@ -58,9 +58,8 @@ private partial def loop : M Bool := do
   modify fun s => { s with modified := false }
   let simprocs := (← get).simprocs
   -- simplify entries
-  let entries := (← get).entries
-  for h : i in [:entries.size] do
-    let entry := entries[i]
+  for i in [:(← get).entries.size] do
+    let entry := (← get).entries[i]!
     let ctx := (← get).ctx
     -- We disable the current entry to prevent it to be simplified to `True`
     let simpThmsWithoutEntry := (← getSimpTheorems).eraseTheorem entry.id

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -146,12 +146,8 @@ def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (
     indexConfig := mkIndexConfig config
   }
 
-def Context.setConfig (context : Context) (config : Config) : MetaM Context := do
-  return { context with
-    config
-    metaConfig := (← mkMetaConfig config)
-    indexConfig := (← mkIndexConfig config)
-  }
+def Context.setConfig (context : Context) (config : Config) : Context :=
+  { context with config }
 
 def Context.setSimpTheorems (c : Context) (simpTheorems : SimpTheoremsArray) : Context :=
   { c with simpTheorems }

src/Lean/Meta/Tactic/Split.lean

@@ -140,8 +140,8 @@ private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : N
           let matcherApp := { matcherApp with discrs := discrVars }
           foundRef.set true
           let mut altsNew := #[]
-          for h : i in [:matcherApp.alts.size] do
-            let alt := matcherApp.alts[i]
+          for i in [:matcherApp.alts.size] do
+            let alt := matcherApp.alts[i]!
             let altNumParams := matcherApp.altNumParams[i]!
             let altNew ← lambdaTelescope alt fun xs body => do
               if xs.size < altNumParams || xs.size < numDiscrEqs then

src/Lean/Meta/Tactic/TryThis.lean

@@ -114,7 +114,7 @@ apply the replacement.
     unless params.range.start.line ≤ stxRange.end.line do return result
     let mut result := result
     for h : i in [:suggestionTexts.size] do
-      let (newText, title?) := suggestionTexts[i]
+      let (newText, title?) := suggestionTexts[i]'h.2
       let title := title?.getD <| (codeActionPrefix?.getD "Try this: ") ++ newText
       result := result.push {
         eager.title := title
@@ -430,13 +430,11 @@ def addSuggestions (ref : Syntax) (suggestions : Array Suggestion)
   logInfoAt ref m!"{header}{msgs}"
   addSuggestionCore ref suggestions header (isInline := false) origSpan? style? codeActionPrefix?
 
-private def addExactSuggestionCore (addSubgoalsMsg : Bool) (e : Expr) : MetaM Suggestion :=
-  withOptions (pp.mvars.set · false) do
+private def addExactSuggestionCore (addSubgoalsMsg : Bool) (e : Expr) : MetaM Suggestion := do
   let stx ← delabToRefinableSyntax e
   let mvars ← getMVars e
   let suggestion ← if mvars.isEmpty then `(tactic| exact $stx) else `(tactic| refine $stx)
-  let pp ← ppExpr e
-  let messageData? := if mvars.isEmpty then m!"exact {pp}" else m!"refine {pp}"
+  let messageData? := if mvars.isEmpty then m!"exact {e}" else m!"refine {e}"
   let postInfo? ← if !addSubgoalsMsg || mvars.isEmpty then pure none else
     let mut str := "\nRemaining subgoals:"
     for g in mvars do

src/Lean/MetavarContext.lean

@@ -248,7 +248,9 @@ instance : Hashable LocalInstance where
 
 /-- Remove local instance with the given `fvarId`. Do nothing if `localInsts` does not contain any free variable with id `fvarId`. -/
 def LocalInstances.erase (localInsts : LocalInstances) (fvarId : FVarId) : LocalInstances :=
-  localInsts.eraseP (fun inst => inst.fvar.fvarId! == fvarId)
+  match localInsts.findIdx? (fun inst => inst.fvar.fvarId! == fvarId) with
+  | some idx => localInsts.eraseIdx idx
+  | _        => localInsts
 
 /-- A kind for the metavariable that determines its unification behaviour.
 For more information see the large comment at the beginning of this file. -/
@@ -1059,7 +1061,7 @@ mutual
 
     Note: It is assumed that `xs` is the result of calling `collectForwardDeps` on a subset of variables in `lctx`.
   -/
-  private partial def mkAuxMVarType (lctx : LocalContext) (xs : Array Expr) (kind : MetavarKind) (e : Expr) (usedLetOnly : Bool) : M Expr := do
+  private partial def mkAuxMVarType (lctx : LocalContext) (xs : Array Expr) (kind : MetavarKind) (e : Expr) : M Expr := do
     let e ← abstractRangeAux xs xs.size e
     xs.size.foldRevM (init := e) fun i e => do
       let x := xs[i]!
@@ -1070,25 +1072,16 @@ mutual
           let type ← abstractRangeAux xs i type
           return Lean.mkForall n bi type e
         | LocalDecl.ldecl _ _ n type value nonDep _ =>
-          if !usedLetOnly || e.hasLooseBVar 0 then
-            let type := type.headBeta
-            let type  ← abstractRangeAux xs i type
-            let value ← abstractRangeAux xs i value
-            let e := mkLet n type value e nonDep
-            match kind with
-            | MetavarKind.syntheticOpaque =>
-              -- See "Gruesome details" section in the beginning of the file
-              let e := e.liftLooseBVars 0 1
-              return mkForall n BinderInfo.default type e
-            | _ => pure e
-          else
-            match kind with
-            | MetavarKind.syntheticOpaque =>
-              let type := type.headBeta
-              let type  ← abstractRangeAux xs i type
-              return mkForall n BinderInfo.default type e
-            | _ =>
-              return e.lowerLooseBVars 1 1
+          let type := type.headBeta
+          let type  ← abstractRangeAux xs i type
+          let value ← abstractRangeAux xs i value
+          let e := mkLet n type value e nonDep
+          match kind with
+          | MetavarKind.syntheticOpaque =>
+            -- See "Gruesome details" section in the beginning of the file
+            let e := e.liftLooseBVars 0 1
+            return mkForall n BinderInfo.default type e
+          | _ => pure e
       else
         -- `xs` may contain metavariables as "may dependencies" (see `findExprDependsOn`)
         let mvarDecl := (← get).mctx.getDecl x.mvarId!
@@ -1108,7 +1101,7 @@ mutual
 
     See details in the comment at the top of the file.
   -/
-  private partial def elimMVar (xs : Array Expr) (mvarId : MVarId) (args : Array Expr) (usedLetOnly : Bool) : M (Expr × Array Expr) := do
+  private partial def elimMVar (xs : Array Expr) (mvarId : MVarId) (args : Array Expr) : M (Expr × Array Expr) := do
     let mvarDecl  := (← getMCtx).getDecl mvarId
     let mvarLCtx  := mvarDecl.lctx
     let toRevert  := getInScope mvarLCtx xs
@@ -1136,7 +1129,7 @@ mutual
       let newMVarLCtx   := reduceLocalContext mvarLCtx toRevert
       let newLocalInsts := mvarDecl.localInstances.filter fun inst => toRevert.all fun x => inst.fvar != x
       -- Remark: we must reset the cache before processing `mkAuxMVarType` because `toRevert` may not be equal to `xs`
-      let newMVarType ← withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type usedLetOnly
+      let newMVarType ← withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type
       let newMVarId    := { name := (← get).ngen.curr }
       let newMVar      := mkMVar newMVarId
       let result       := mkMVarApp mvarLCtx newMVar toRevert newMVarKind
@@ -1177,8 +1170,7 @@ mutual
         if (← read).mvarIdsToAbstract.contains mvarId then
           return mkAppN f (← args.mapM (visit xs))
         else
-          -- We set `usedLetOnly := true` to avoid unnecessary let binders in the new metavariable type.
-          return (← elimMVar xs mvarId args (usedLetOnly := true)).1
+          return (← elimMVar xs mvarId args).1
     | _ =>
       return mkAppN (← visit xs f) (← args.mapM (visit xs))
 
@@ -1200,9 +1192,7 @@ partial def elimMVarDeps (xs : Array Expr) (e : Expr) : M Expr :=
 -/
 partial def revert (xs : Array Expr) (mvarId : MVarId) : M (Expr × Array Expr) :=
   withFreshCache do
-    -- We set `usedLetOnly := false`, because in the `revert` tactic
-    -- we expect that reverting a let variable always results in a let binder.
-    elimMVar xs mvarId #[] (usedLetOnly := false)
+    elimMVar xs mvarId #[]
 
 /--
   Similar to `Expr.abstractRange`, but handles metavariables correctly.

src/Lean/Parser/Command.lean

@@ -137,7 +137,7 @@ def declValEqns      := leading_parser
 def whereStructField := leading_parser
   Term.letDecl
 def whereStructInst  := leading_parser
-  ppIndent ppSpace >> "where" >> Term.structInstFields (sepByIndent (ppGroup whereStructField) "; " (allowTrailingSep := true)) >>
+  ppIndent ppSpace >> "where" >> sepByIndent (ppGroup whereStructField) "; " (allowTrailingSep := true) >>
   optional Term.whereDecls
 /-- `declVal` matches the right-hand side of a declaration, one of:
 * `:= expr` (a "simple declaration")

src/Lean/Parser/Term.lean

@@ -281,12 +281,6 @@ def structInstFieldAbbrev := leading_parser
   atomic (ident >> notFollowedBy ("." <|> ":=" <|> symbol "[") "invalid field abbreviation")
 def optEllipsis      := leading_parser
   optional " .."
-/-
-Tags the structure instance field syntax with a `Lean.Parser.Term.structInstFields` syntax node.
-This node is used to enable structure instance field completion in the whitespace
-of a structure instance notation.
--/
-def structInstFields (p : Parser) : Parser := node `Lean.Parser.Term.structInstFields p
 /--
 Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
 inherited. If `e` is itself a variable called `x`, it can be elided:
@@ -298,7 +292,7 @@ The structure type can be specified if not inferable:
 -/
 @[builtin_term_parser] def structInst := leading_parser
   "{ " >> withoutPosition (optional (atomic (sepBy1 termParser ", " >> " with "))
-    >> structInstFields (sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true))
+    >> sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true)
     >> optEllipsis
     >> optional (" : " >> termParser)) >> " }"
 def typeSpec := leading_parser " : " >> termParser
@@ -990,7 +984,6 @@ builtin_initialize
   register_parser_alias bracketedBinder
   register_parser_alias attrKind
   register_parser_alias optSemicolon
-  register_parser_alias structInstFields
 
 end Parser
 end Lean

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -91,32 +91,21 @@ Rather, it is called through the `app` delaborator.
 -/
 def delabConst : Delab := do
   let Expr.const c₀ ls ← getExpr | unreachable!
-  let mut c₀ := c₀
-  let mut c  := c₀
-  if let some n := privateToUserName? c₀ then
-    unless (← getPPOption getPPPrivateNames) do
-      if c₀ == mkPrivateName (← getEnv) n then
-        -- The name is defined in this module, so use `n` as the name and unresolve like any other name.
-        c₀ := n
-        c ← unresolveNameGlobal n (fullNames := ← getPPOption getPPFullNames)
+  let c₀ := if (← getPPOption getPPPrivateNames) then c₀ else (privateToUserName? c₀).getD c₀
+
+  let mut c ← unresolveNameGlobal c₀ (fullNames := ← getPPOption getPPFullNames)
+  let stx ← if ls.isEmpty || !(← getPPOption getPPUniverses) then
+    if (← getLCtx).usesUserName c then
+      -- `c` is also a local declaration
+      if c == c₀ && !(← read).inPattern then
+        -- `c` is the fully qualified named. So, we append the `_root_` prefix
+        c := `_root_ ++ c
       else
-        -- The name is not defined in this module, so make inaccessible. Unresolving does not make sense to do.
-        c ← withFreshMacroScope <| MonadQuotation.addMacroScope n
+        c := c₀
+    pure <| mkIdent c
   else
-    c ← unresolveNameGlobal c (fullNames := ← getPPOption getPPFullNames)
-  let stx ←
-    if ls.isEmpty || !(← getPPOption getPPUniverses) then
-      if (← getLCtx).usesUserName c then
-        -- `c` is also a local declaration
-        if c == c₀ && !(← read).inPattern then
-          -- `c` is the fully qualified named. So, we append the `_root_` prefix
-          c := `_root_ ++ c
-        else
-          c := c₀
-      pure <| mkIdent c
-    else
-      let mvars ← getPPOption getPPMVarsLevels
-      `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*})
+    let mvars ← getPPOption getPPMVarsLevels
+    `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*})
 
   let stx ← maybeAddBlockImplicit stx
   if (← getPPOption getPPTagAppFns) then
@@ -349,7 +338,7 @@ def delabAppExplicitCore (fieldNotation : Bool) (numArgs : Nat) (delabHead : (in
     if idx == 0 then
       -- If it's the first argument, then we can tag `obj.field` with the first app.
       head ← withBoundedAppFn (numArgs - 1) <| annotateTermInfo head
-    return Syntax.mkApp head (argStxs.eraseIdxIfInBounds idx)
+    return Syntax.mkApp head (argStxs.eraseIdx idx)
   else
     return Syntax.mkApp fnStx argStxs
 
@@ -876,7 +865,7 @@ def delabLam : Delab :=
           -- "default" binder group is the only one that expects binder names
           -- as a term, i.e. a single `Syntax.ident` or an application thereof
           let stxCurNames ←
-            if h : curNames.size > 1 then
+            if curNames.size > 1 then
               `($(curNames.get! 0) $(curNames.eraseIdx 0)*)
             else
               pure $ curNames.get! 0;

src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean

@@ -57,8 +57,8 @@ private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name ×
   -- Search for the first argument that could be used for field notation
   -- and make sure it is the first explicit argument.
   forallBoundedTelescope info.type args.size fun params _ => do
-    for h : i in [0:params.size] do
-      let fvarId := params[i].fvarId!
+    for i in [0:params.size] do
+      let fvarId := params[i]!.fvarId!
       -- If there is a motive, we will treat this as a sort of control flow structure and so we won't use field notation.
       -- Plus, recursors tend to be riskier when using dot notation.
       if (← fvarId.getUserName) == `motive then

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -308,12 +308,12 @@ partial def canBottomUp (e : Expr) (mvar? : Option Expr := none) (fuel : Nat :=
     let args := e.getAppArgs
     let fType ← replaceLPsWithVars (← inferType e.getAppFn)
     let (mvars, bInfos, resultType) ← forallMetaBoundedTelescope fType e.getAppArgs.size
-    for h : i in [:mvars.size] do
+    for i in [:mvars.size] do
       if bInfos[i]! == BinderInfo.instImplicit then
-        inspectOutParams args[i]! mvars[i]
+        inspectOutParams args[i]! mvars[i]!
       else if bInfos[i]! == BinderInfo.default then
-        if ← isTrivialBottomUp args[i]! then tryUnify args[i]! mvars[i]
-        else if ← typeUnknown mvars[i] <&&> canBottomUp args[i]! (some mvars[i]) fuel then tryUnify args[i]! mvars[i]
+        if ← isTrivialBottomUp args[i]! then tryUnify args[i]! mvars[i]!
+        else if ← typeUnknown mvars[i]! <&&> canBottomUp args[i]! (some mvars[i]!) fuel then tryUnify args[i]! mvars[i]!
     if ← (pure (isHBinOp e) <&&> (valUnknown mvars[0]! <||> valUnknown mvars[1]!)) then tryUnify mvars[0]! mvars[1]!
     if mvar?.isSome then tryUnify resultType (← inferType mvar?.get!)
     return !(← valUnknown resultType)
@@ -487,22 +487,22 @@ mutual
     collectBottomUps := do
       let { args, mvars, bInfos, ..} ← read
       for target in [fun _ => none, fun i => some mvars[i]!] do
-        for h : i in [:args.size] do
+        for i in [:args.size] do
           if bInfos[i]! == BinderInfo.default then
-            if ← typeUnknown mvars[i]! <&&> canBottomUp args[i] (target i) then
+            if ← typeUnknown mvars[i]! <&&> canBottomUp args[i]! (target i) then
               tryUnify args[i]! mvars[i]!
               modify fun s => { s with bottomUps := s.bottomUps.set! i true }
 
     checkOutParams := do
       let { args, mvars, bInfos, ..} ← read
-      for h : i in [:args.size] do
-        if bInfos[i]! == BinderInfo.instImplicit then inspectOutParams args[i] mvars[i]!
+      for i in [:args.size] do
+        if bInfos[i]! == BinderInfo.instImplicit then inspectOutParams args[i]! mvars[i]!
 
     collectHigherOrders := do
       let { args, mvars, bInfos, ..} ← read
-      for h : i in [:args.size] do
+      for i in [:args.size] do
         if !(bInfos[i]! == BinderInfo.implicit || bInfos[i]! == BinderInfo.strictImplicit) then continue
-        if !(← isHigherOrder (← inferType args[i])) then continue
+        if !(← isHigherOrder (← inferType args[i]!)) then continue
         if getPPAnalyzeTrustId (← getOptions) && isIdLike args[i]! then continue
 
         if getPPAnalyzeTrustKnownFOType2TypeHOFuns (← getOptions) && !(← valUnknown mvars[i]!)
@@ -520,9 +520,9 @@ mutual
       -- motivation: prevent levels from printing in
       -- Boo.mk : {α : Type u_1} → {β : Type u_2} → α → β → Boo.{u_1, u_2} α β
       let { args, mvars, bInfos, ..} ← read
-      for h : i in [:args.size] do
+      for i in [:args.size] do
         if bInfos[i]! == BinderInfo.default then
-          if ← valUnknown mvars[i]! <&&> isTrivialBottomUp args[i] then
+          if ← valUnknown mvars[i]! <&&> isTrivialBottomUp args[i]! then
             tryUnify args[i]! mvars[i]!
             modify fun s => { s with bottomUps := s.bottomUps.set! i true }
 

src/Lean/Server/Completion/CompletionCollectors.lean

@@ -1,610 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Marc Huisinga
--/
-prelude
-import Lean.Data.FuzzyMatching
-import Lean.Elab.Tactic.Doc
-import Lean.Server.Completion.CompletionResolution
-import Lean.Server.Completion.EligibleHeaderDecls
-
-namespace Lean.Server.Completion
-open Elab
-open Lean.Lsp
-open Meta
-open FuzzyMatching
-
-section Infrastructure
-
-  structure ScoredCompletionItem where
-    item  : CompletionItem
-    score : Float
-    deriving Inhabited
-
-  private structure Context where
-    params            : CompletionParams
-    completionInfoPos : Nat
-
-
-  /-- Intermediate state while completions are being computed. -/
-  private structure State where
-    /-- All completion items and their fuzzy match scores so far. -/
-    items  : Array ScoredCompletionItem := #[]
-
-  /--
-  Monad used for completion computation that allows modifying a completion `State` and reading
-  `CompletionParams`.
-  -/
-  private abbrev M := ReaderT Context $ StateRefT State MetaM
-
-  /-- Adds a new completion item to the state in `M`. -/
-  private def addItem
-      (item  : CompletionItem)
-      (score : Float)
-      (id?   : Option CompletionIdentifier := none)
-      : M Unit := do
-    let ctx ← read
-    let data := {
-      params := ctx.params,
-      cPos := ctx.completionInfoPos,
-      id?
-      : ResolvableCompletionItemData
-    }
-    let item := { item with data? := toJson data }
-    modify fun s => { s with items := s.items.push ⟨item, score⟩ }
-
-  /--
-  Adds a new completion item with the given `label`, `id`, `kind` and `score` to the state in `M`.
-  Computes the doc string from the environment if available.
-  -/
-  private def addUnresolvedCompletionItem
-      (label         : Name)
-      (id            : CompletionIdentifier)
-      (kind          : CompletionItemKind)
-      (score         : Float)
-      : M Unit := do
-    let env ← getEnv
-    let (docStringPrefix?, tags?) := Id.run do
-      let .const declName := id
-        | (none, none)
-      let some param := Linter.deprecatedAttr.getParam? env declName
-        | (none, none)
-      let docstringPrefix :=
-        if let some text := param.text? then
-          text
-        else if let some newName := param.newName? then
-          s!"`{declName}` has been deprecated, use `{newName}` instead."
-        else
-          s!"`{declName}` has been deprecated."
-      (some docstringPrefix, some #[CompletionItemTag.deprecated])
-    let docString? ← do
-      let .const declName := id
-        | pure none
-      findDocString? env declName
-    let doc? := do
-      let docValue ←
-        match docStringPrefix?, docString? with
-        | none,                 none           => none
-        | some docStringPrefix, none           => docStringPrefix
-        | none,                 docString      => docString
-        | some docStringPrefix, some docString => s!"{docStringPrefix}\n\n{docString}"
-      pure { value := docValue , kind := MarkupKind.markdown : MarkupContent }
-    let item := { label := label.toString, kind? := kind, documentation? := doc?, tags?}
-    addItem item score id
-
-  private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionItemKind := do
-    let env ← getEnv
-    if constInfo.isCtor then
-      return CompletionItemKind.constructor
-    else if constInfo.isInductive then
-      if isClass env constInfo.name then
-        return CompletionItemKind.class
-      else if (← isEnumType constInfo.name) then
-        return CompletionItemKind.enum
-      else
-        return CompletionItemKind.struct
-    else if constInfo.isTheorem then
-      return CompletionItemKind.event
-    else if (← isProjectionFn constInfo.name) then
-      return CompletionItemKind.field
-    else
-      let isFunction : Bool ← withTheReader Core.Context ({ · with maxHeartbeats := 0 }) do
-        return (← whnf constInfo.type).isForall
-      if isFunction then
-        return CompletionItemKind.function
-      else
-        return CompletionItemKind.constant
-
-  private def addUnresolvedCompletionItemForDecl (label : Name) (declName : Name) (score : Float) : M Unit := do
-    if let some c := (← getEnv).find? declName then
-      addUnresolvedCompletionItem label (.const declName) (← getCompletionKindForDecl c) score
-
-  private def addKeywordCompletionItem (keyword : String) (score : Float) : M Unit := do
-    let item := { label := keyword, detail? := "keyword", documentation? := none, kind? := CompletionItemKind.keyword }
-    addItem item score
-
-  private def addNamespaceCompletionItem (ns : Name) (score : Float) : M Unit := do
-    let item := { label := ns.toString, detail? := "namespace", documentation? := none, kind? := CompletionItemKind.module }
-    addItem item score
-
-  private def runM
-      (params            : CompletionParams)
-      (completionInfoPos : Nat)
-      (ctx               : ContextInfo)
-      (lctx              : LocalContext)
-      (x                 : M Unit)
-      : IO (Array ScoredCompletionItem) :=
-    ctx.runMetaM lctx do
-      let (_, s) ← x.run ⟨params, completionInfoPos⟩ |>.run {}
-      return s.items
-
-end Infrastructure
-
-section Utils
-
-  private def normPrivateName? (declName : Name) : MetaM (Option Name) := do
-    match privateToUserName? declName with
-    | none => return declName
-    | some userName =>
-      if mkPrivateName (← getEnv) userName == declName then
-        return userName
-      else
-        return none
-
-  /--
-    Return the auto-completion label if `id` can be auto completed using `declName` assuming namespace `ns` is open.
-    This function only succeeds with atomic labels. BTW, it seems most clients only use the last part.
-
-    Remark: `danglingDot == true` when the completion point is an identifier followed by `.`.
-  -/
-  private def matchDecl? (ns : Name) (id : Name) (danglingDot : Bool) (declName : Name) : MetaM (Option (Name × Float)) := do
-    let some declName ← normPrivateName? declName
-      | return none
-    if !ns.isPrefixOf declName then
-      return none
-    let declName := declName.replacePrefix ns Name.anonymous
-    if danglingDot then
-      -- If the input is `id.` and `declName` is of the form `id.atomic`, complete with `atomicName`
-      if id.isPrefixOf declName then
-        let declName := declName.replacePrefix id Name.anonymous
-        if declName.isAtomic && !declName.isAnonymous then
-          return some (declName, 1)
-    else if let (.str p₁ s₁, .str p₂ s₂) := (id, declName) then
-      if p₁ == p₂ then
-        -- If the namespaces agree, fuzzy-match on the trailing part
-        return fuzzyMatchScoreWithThreshold? s₁ s₂ |>.map (.mkSimple s₂, ·)
-      else if p₁.isAnonymous then
-        -- If `id` is namespace-less, also fuzzy-match declaration names in arbitrary namespaces
-        -- (but don't match the namespace itself).
-        -- Penalize score by component length of added namespace.
-        return fuzzyMatchScoreWithThreshold? s₁ s₂ |>.map (declName, · / (p₂.getNumParts + 1).toFloat)
-    return none
-
-end Utils
-
-section IdCompletionUtils
-
-  private def matchAtomic (id : Name) (declName : Name) (danglingDot : Bool) : Option Float := do
-    if danglingDot then
-      none
-    match id, declName with
-    | .str .anonymous s₁, .str .anonymous s₂ => fuzzyMatchScoreWithThreshold? s₁ s₂
-    | _, _ => none
-
-  /--
-  Truncate the given identifier and make sure it has length `≤ newLength`.
-  This function assumes `id` does not contain `Name.num` constructors.
-  -/
-  private partial def truncate (id : Name) (newLen : Nat) : Name :=
-    let rec go (id : Name) : Name × Nat :=
-      match id with
-      | Name.anonymous => (id, 0)
-      | Name.num ..    => unreachable!
-      | .str p s =>
-        let (p', len) := go p
-        if len + 1 >= newLen then
-          (p', len)
-        else
-          let optDot := if p.isAnonymous then 0 else 1
-          let len'   := len + optDot + s.length
-          if len' ≤ newLen then
-            (id, len')
-          else
-            (Name.mkStr p (s.extract 0 ⟨newLen - optDot - len⟩), newLen)
-    (go id).1
-
-  def matchNamespace (ns : Name) (nsFragment : Name) (danglingDot : Bool) : Option Float :=
-    if danglingDot then
-      if nsFragment != ns && nsFragment.isPrefixOf ns then
-        some 1
-      else
-        none
-    else
-      match ns, nsFragment with
-      | .str p₁ s₁, .str p₂ s₂ =>
-        if p₁ == p₂ then fuzzyMatchScoreWithThreshold? s₂ s₁ else none
-      | _, _ => none
-
-  def completeNamespaces (ctx : ContextInfo) (id : Name) (danglingDot : Bool) : M Unit := do
-    let env ← getEnv
-    let add (ns : Name) (ns' : Name) (score : Float) : M Unit :=
-      if danglingDot then
-        addNamespaceCompletionItem (ns.replacePrefix (ns' ++ id) Name.anonymous) score
-      else
-        addNamespaceCompletionItem (ns.replacePrefix ns' Name.anonymous) score
-    env.getNamespaceSet |>.forM fun ns => do
-      unless ns.isInternal || env.contains ns do -- Ignore internal and namespaces that are also declaration names
-        for openDecl in ctx.openDecls do
-          match openDecl with
-          | OpenDecl.simple ns' _      =>
-            if let some score := matchNamespace ns (ns' ++ id) danglingDot then
-              add ns ns' score
-              return ()
-          | _ => pure ()
-        -- use current namespace
-        let rec visitNamespaces (ns' : Name) : M Unit := do
-          if let some score := matchNamespace ns (ns' ++ id) danglingDot then
-            add ns ns' score
-          else
-            match ns' with
-            | Name.str p .. => visitNamespaces p
-            | _ => return ()
-        visitNamespaces ctx.currNamespace
-
-end IdCompletionUtils
-
-section DotCompletionUtils
-
-  private def unfoldeDefinitionGuarded? (e : Expr) : MetaM (Option Expr) :=
-    try unfoldDefinition? e catch _ => pure none
-
-  /-- Return `true` if `e` is a `declName`-application, or can be unfolded (delta-reduced) to one. -/
-  private partial def isDefEqToAppOf (e : Expr) (declName : Name) : MetaM Bool := do
-    let isConstOf := match e.getAppFn with
-      | .const name .. => (privateToUserName? name).getD name == declName
-      | _ => false
-    if isConstOf then
-      return true
-    let some e ← unfoldeDefinitionGuarded? e | return false
-    isDefEqToAppOf e declName
-
-  private def isDotCompletionMethod (typeName : Name) (info : ConstantInfo) : MetaM Bool :=
-    forallTelescopeReducing info.type fun xs _ => do
-      for x in xs do
-        let localDecl ← x.fvarId!.getDecl
-        let type := localDecl.type.consumeMData
-        if (← isDefEqToAppOf type typeName) then
-          return true
-      return false
-
-  /--
-  Checks whether the expected type of `info.type` can be reduced to an application of `typeName`.
-  -/
-  private def isDotIdCompletionMethod (typeName : Name) (info : ConstantInfo) : MetaM Bool := do
-    forallTelescopeReducing info.type fun _ type =>
-      isDefEqToAppOf type.consumeMData typeName
-
-  /--
-  Converts `n` to `Name.anonymous` if `n` is a private prefix (see `Lean.isPrivatePrefix`).
-  -/
-  private def stripPrivatePrefix (n : Name) : Name :=
-    match n with
-    | .num _ 0 => if isPrivatePrefix n then .anonymous else n
-    | _ => n
-
-  /--
-  Compares `n₁` and `n₂` modulo private prefixes. Similar to `Name.cmp` but ignores all
-  private prefixes in both names.
-  Necessary because the namespaces of private names do not contain private prefixes.
-  -/
-  private partial def cmpModPrivate (n₁ n₂ : Name) : Ordering :=
-    let n₁ := stripPrivatePrefix n₁
-    let n₂ := stripPrivatePrefix n₂
-    match n₁, n₂ with
-    | .anonymous, .anonymous => Ordering.eq
-    | .anonymous, _          => Ordering.lt
-    | _,          .anonymous => Ordering.gt
-    | .num p₁ i₁, .num p₂ i₂ =>
-      match compare i₁ i₂ with
-      | Ordering.eq => cmpModPrivate p₁ p₂
-      | ord         => ord
-    | .num _ _,   .str _ _   => Ordering.lt
-    | .str _ _,   .num _ _   => Ordering.gt
-    | .str p₁ n₁, .str p₂ n₂ =>
-      match compare n₁ n₂ with
-      | Ordering.eq => cmpModPrivate p₁ p₂
-      | ord         => ord
-
-  /--
-  `NameSet` where names are compared according to `cmpModPrivate`.
-  Helps speed up dot completion because it allows us to look up names without first having to
-  strip the private prefix from deep in the name, letting us reject most names without
-  having to scan the full name first.
-  -/
-  private def NameSetModPrivate := RBTree Name cmpModPrivate
-
-  /--
-    Given a type, try to extract relevant type names for dot notation field completion.
-    We extract the type name, parent struct names, and unfold the type.
-    The process mimics the dot notation elaboration procedure at `App.lean` -/
-  private partial def getDotCompletionTypeNames (type : Expr) : MetaM NameSetModPrivate :=
-    return (← visit type |>.run RBTree.empty).2
-  where
-    visit (type : Expr) : StateRefT NameSetModPrivate MetaM Unit := do
-      let .const typeName _ := type.getAppFn | return ()
-      modify fun s => s.insert typeName
-      if isStructure (← getEnv) typeName then
-        for parentName in (← getAllParentStructures typeName) do
-          modify fun s => s.insert parentName
-      let some type ← unfoldeDefinitionGuarded? type | return ()
-      visit type
-
-end DotCompletionUtils
-
-private def idCompletionCore
-    (ctx         : ContextInfo)
-    (stx         : Syntax)
-    (id          : Name)
-    (hoverInfo   : HoverInfo)
-    (danglingDot : Bool)
-    : M Unit := do
-  let mut id := id
-  if id.hasMacroScopes then
-    if stx.getHeadInfo matches .original .. then
-      id := id.eraseMacroScopes
-    else
-      -- Identifier is synthetic and has macro scopes => no completions
-      -- Erasing the macro scopes does not make sense in this case because the identifier name
-      -- is some random synthetic string.
-      return
-  let mut danglingDot := danglingDot
-  if let HoverInfo.inside delta := hoverInfo then
-    id := truncate id delta
-    danglingDot := false
-  if id.isAtomic then
-    -- search for matches in the local context
-    for localDecl in (← getLCtx) do
-      if let some score := matchAtomic id localDecl.userName danglingDot then
-        addUnresolvedCompletionItem localDecl.userName (.fvar localDecl.fvarId) (kind := CompletionItemKind.variable) score
-  -- search for matches in the environment
-  let env ← getEnv
-  forEligibleDeclsM fun declName c => do
-    let bestMatch? ← (·.2) <$> StateT.run (s := none) do
-      let matchUsingNamespace (ns : Name) : StateT (Option (Name × Float)) M Unit := do
-        let some (label, score) ← matchDecl? ns id danglingDot declName
-          | return
-        modify fun
-          | none =>
-            some (label, score)
-          | some (bestLabel, bestScore) =>
-            -- for open namespaces `A` and `A.B` and a decl `A.B.c`, pick the decl `c` over `B.c`
-            if label.isSuffixOf bestLabel then
-              some (label, score)
-            else
-              some (bestLabel, bestScore)
-      let rec visitNamespaces (ns : Name) : StateT (Option (Name × Float)) M Unit := do
-        let Name.str p .. := ns
-          | return ()
-        matchUsingNamespace ns
-        visitNamespaces p
-      -- use current namespace
-      visitNamespaces ctx.currNamespace
-      -- use open decls
-      for openDecl in ctx.openDecls do
-        let OpenDecl.simple ns exs := openDecl
-          | pure ()
-        if exs.contains declName then
-          continue
-        matchUsingNamespace ns
-      matchUsingNamespace Name.anonymous
-    if let some (bestLabel, bestScore) := bestMatch? then
-      addUnresolvedCompletionItem bestLabel (.const declName) (← getCompletionKindForDecl c) bestScore
-  let matchAlias (ns : Name) (alias : Name) : Option Float :=
-    -- Recall that aliases may not be atomic and include the namespace where they were created.
-    if ns.isPrefixOf alias then
-      let alias := alias.replacePrefix ns Name.anonymous
-      matchAtomic id alias danglingDot
-    else
-      none
-  let eligibleHeaderDecls ← getEligibleHeaderDecls env
-  -- Auxiliary function for `alias`
-  let addAlias (alias : Name) (declNames : List Name) (score : Float) : M Unit := do
-    declNames.forM fun declName => do
-      if allowCompletion eligibleHeaderDecls env declName then
-        addUnresolvedCompletionItemForDecl (.mkSimple alias.getString!) declName score
-  -- search explicitly open `ids`
-  for openDecl in ctx.openDecls do
-    match openDecl with
-    | OpenDecl.explicit openedId resolvedId =>
-      if allowCompletion eligibleHeaderDecls env resolvedId then
-        if let some score := matchAtomic id openedId danglingDot then
-          addUnresolvedCompletionItemForDecl (.mkSimple openedId.getString!) resolvedId score
-    | OpenDecl.simple ns _      =>
-      getAliasState env |>.forM fun alias declNames => do
-        if let some score := matchAlias ns alias then
-          addAlias alias declNames score
-  -- search for aliases
-  getAliasState env |>.forM fun alias declNames => do
-    -- use current namespace
-    let rec searchAlias (ns : Name) : M Unit := do
-      if let some score := matchAlias ns alias then
-        addAlias alias declNames score
-      else
-        match ns with
-        | Name.str p ..  => searchAlias p
-        | _ => return ()
-    searchAlias ctx.currNamespace
-  -- Search keywords
-  if !danglingDot then
-    if let .str .anonymous s := id then
-      let keywords := Parser.getTokenTable env
-      for keyword in keywords.findPrefix s do
-        if let some score := fuzzyMatchScoreWithThreshold? s keyword then
-          addKeywordCompletionItem keyword score
-  -- Search namespaces
-  completeNamespaces ctx id danglingDot
-
-def idCompletion
-    (params            : CompletionParams)
-    (completionInfoPos : Nat)
-    (ctx               : ContextInfo)
-    (lctx              : LocalContext)
-    (stx               : Syntax)
-    (id                : Name)
-    (hoverInfo         : HoverInfo)
-    (danglingDot       : Bool)
-    : IO (Array ScoredCompletionItem) :=
-  runM params completionInfoPos ctx lctx do
-    idCompletionCore ctx stx id hoverInfo danglingDot
-
-def dotCompletion
-    (params            : CompletionParams)
-    (completionInfoPos : Nat)
-    (ctx               : ContextInfo)
-    (info              : TermInfo)
-    : IO (Array ScoredCompletionItem) :=
-  runM params completionInfoPos ctx info.lctx do
-    let nameSet ← try
-      getDotCompletionTypeNames (← instantiateMVars (← inferType info.expr))
-    catch _ =>
-      pure RBTree.empty
-    if nameSet.isEmpty then
-      return
-
-    forEligibleDeclsM fun declName c => do
-      let unnormedTypeName := declName.getPrefix
-      if ! nameSet.contains unnormedTypeName then
-        return
-      let some declName ← normPrivateName? declName
-        | return
-      let typeName := declName.getPrefix
-      if ! (← isDotCompletionMethod typeName c) then
-        return
-      let completionKind ← getCompletionKindForDecl c
-      addUnresolvedCompletionItem (.mkSimple c.name.getString!) (.const c.name) (kind := completionKind) 1
-
-def dotIdCompletion
-    (params            : CompletionParams)
-    (completionInfoPos : Nat)
-    (ctx               : ContextInfo)
-    (lctx              : LocalContext)
-    (id                : Name)
-    (expectedType?     : Option Expr)
-    : IO (Array ScoredCompletionItem) :=
-  runM params completionInfoPos ctx lctx do
-    let some expectedType := expectedType?
-      | return ()
-
-    let resultTypeFn := (← instantiateMVars expectedType).cleanupAnnotations.getAppFn.cleanupAnnotations
-    let .const .. := resultTypeFn
-      | return ()
-
-    let nameSet ← try
-      getDotCompletionTypeNames resultTypeFn
-    catch _ =>
-      pure RBTree.empty
-
-    forEligibleDeclsM fun declName c => do
-      let unnormedTypeName := declName.getPrefix
-      if ! nameSet.contains unnormedTypeName then
-        return
-
-      let some declName ← normPrivateName? declName
-        | return
-
-      let typeName := declName.getPrefix
-      if ! (← isDotIdCompletionMethod typeName c) then
-        return
-
-      let completionKind ← getCompletionKindForDecl c
-      if id.isAnonymous then
-        -- We're completing a lone dot => offer all decls of the type
-        addUnresolvedCompletionItem (.mkSimple c.name.getString!) (.const c.name) completionKind 1
-        return
-
-      let some (label, score) ← matchDecl? typeName id (danglingDot := false) declName | pure ()
-      addUnresolvedCompletionItem label (.const c.name) completionKind score
-
-def fieldIdCompletion
-    (params            : CompletionParams)
-    (completionInfoPos : Nat)
-    (ctx               : ContextInfo)
-    (lctx              : LocalContext)
-    (id                : Option Name)
-    (structName        : Name)
-    : IO (Array ScoredCompletionItem) :=
-  runM params completionInfoPos ctx lctx do
-    let idStr := id.map (·.toString) |>.getD ""
-    let fieldNames := getStructureFieldsFlattened (← getEnv) structName (includeSubobjectFields := false)
-    for fieldName in fieldNames do
-      let .str _ fieldName := fieldName | continue
-      let some score := fuzzyMatchScoreWithThreshold? idStr fieldName | continue
-      let item := { label := fieldName, detail? := "field", documentation? := none, kind? := CompletionItemKind.field }
-      addItem item score
-
-def optionCompletion
-    (params            : CompletionParams)
-    (completionInfoPos : Nat)
-    (ctx               : ContextInfo)
-    (stx               : Syntax)
-    (caps              : ClientCapabilities)
-    : IO (Array ScoredCompletionItem) :=
-  ctx.runMetaM {} do
-    let (partialName, trailingDot) :=
-      -- `stx` is from `"set_option" >> ident`
-      match stx[1].getSubstring? (withLeading := false) (withTrailing := false) with
-      | none => ("", false)  -- the `ident` is `missing`, list all options
-      | some ss =>
-        if !ss.str.atEnd ss.stopPos && ss.str.get ss.stopPos == '.' then
-          -- include trailing dot, which is not parsed by `ident`
-          (ss.toString ++ ".", true)
-        else
-          (ss.toString, false)
-    -- HACK(WN): unfold the type so ForIn works
-    let (decls : RBMap _ _ _) ← getOptionDecls
-    let opts ← getOptions
-    let mut items := #[]
-    for ⟨name, decl⟩ in decls do
-      if let some score := fuzzyMatchScoreWithThreshold? partialName name.toString then
-        let textEdit :=
-          if !caps.textDocument?.any (·.completion?.any (·.completionItem?.any (·.insertReplaceSupport?.any (·)))) then
-            none -- InsertReplaceEdit not supported by client
-          else if let some ⟨start, stop⟩ := stx[1].getRange? then
-            let stop := if trailingDot then stop + ' ' else stop
-            let range := ⟨ctx.fileMap.utf8PosToLspPos start, ctx.fileMap.utf8PosToLspPos stop⟩
-            some { newText := name.toString, insert := range, replace := range : InsertReplaceEdit }
-          else
-            none
-        items := items.push ⟨{
-            label := name.toString
-            detail? := s!"({opts.get name decl.defValue}), {decl.descr}"
-            documentation? := none,
-            kind? := CompletionItemKind.property -- TODO: investigate whether this is the best kind for options.
-            textEdit? := textEdit
-            data? := toJson {
-              params,
-              cPos := completionInfoPos,
-              id? := none : ResolvableCompletionItemData
-            }
-          }, score⟩
-    return items
-
-def tacticCompletion
-    (params            : CompletionParams)
-    (completionInfoPos : Nat)
-    (ctx               : ContextInfo)
-    : IO (Array ScoredCompletionItem) := ctx.runMetaM .empty do
-  let allTacticDocs ← Tactic.Doc.allTacticDocs
-  let items : Array ScoredCompletionItem := allTacticDocs.map fun tacticDoc =>
-    ⟨{
-      label          := tacticDoc.userName
-      detail?        := none
-      documentation? := tacticDoc.docString.map fun docString =>
-        { value := docString, kind := MarkupKind.markdown : MarkupContent }
-      kind?          := CompletionItemKind.keyword
-      data?          := toJson { params, cPos := completionInfoPos, id? := none : ResolvableCompletionItemData }
-    }, 1⟩
-  return items
-
-end Lean.Server.Completion

src/Lean/Server/Completion/CompletionInfoSelection.lean

@@ -1,131 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Marc Huisinga
--/
-prelude
-import Lean.Server.Completion.SyntheticCompletion
-
-namespace Lean.Server.Completion
-open Elab
-
-private def filterDuplicateCompletionInfos
-    (infos : Array ContextualizedCompletionInfo)
-    : Array ContextualizedCompletionInfo := Id.run do
-  -- We don't expect there to be too many duplicate completion infos,
-  -- so it's fine if this is quadratic (we don't need to implement `Hashable` / `LT` this way).
-  let mut deduplicatedInfos : Array ContextualizedCompletionInfo := #[]
-  for i in infos do
-    if deduplicatedInfos.any (fun di => eq di.info i.info) then
-      continue
-    deduplicatedInfos := deduplicatedInfos.push i
-  deduplicatedInfos
-where
-  eq : CompletionInfo → CompletionInfo → Bool
-    | .dot ti₁ .., .dot ti₂ .. =>
-      ti₁.stx.eqWithInfo ti₂.stx && ti₁.expr == ti₂.expr
-    | .id stx₁ id₁ .., .id stx₂ id₂ .. =>
-      stx₁.eqWithInfo stx₂ && id₁ == id₂
-    | .dotId stx₁ id₁ .., .id stx₂ id₂ .. =>
-      stx₁.eqWithInfo stx₂ && id₁ == id₂
-    | .fieldId stx₁ id₁? _ structName₁, .fieldId stx₂ id₂? _ structName₂ =>
-      stx₁.eqWithInfo stx₂ && id₁? == id₂? && structName₁ == structName₂
-    | .namespaceId stx₁, .namespaceId stx₂ =>
-      stx₁.eqWithInfo stx₂
-    | .option stx₁, .option stx₂ =>
-      stx₁.eqWithInfo stx₂
-    | .endSection stx₁ scopeNames₁, .endSection stx₂ scopeNames₂ =>
-      stx₁.eqWithInfo stx₂ && scopeNames₁ == scopeNames₂
-    | .tactic stx₁, .tactic stx₂ =>
-      stx₁.eqWithInfo stx₂
-    | _, _ =>
-      false
-
-def findCompletionInfosAt
-    (fileMap  : FileMap)
-    (hoverPos : String.Pos)
-    (cmdStx   : Syntax)
-    (infoTree : InfoTree)
-    : Array ContextualizedCompletionInfo := Id.run do
-  let ⟨hoverLine, _⟩ := fileMap.toPosition hoverPos
-  let mut completionInfoCandidates := infoTree.foldInfo (init := #[]) (go hoverLine)
-  if completionInfoCandidates.isEmpty then
-    completionInfoCandidates := findSyntheticCompletions fileMap hoverPos cmdStx infoTree
-  return filterDuplicateCompletionInfos completionInfoCandidates
-where
-  go
-      (hoverLine : Nat)
-      (ctx       : ContextInfo)
-      (info      : Info)
-      (best     : Array ContextualizedCompletionInfo)
-      : Array ContextualizedCompletionInfo := Id.run do
-    let .ofCompletionInfo completionInfo := info
-      | return best
-    if ! info.occursInOrOnBoundary hoverPos then
-      return best
-    let headPos := info.pos?.get!
-    let tailPos := info.tailPos?.get!
-    let hoverInfo :=
-      if hoverPos < tailPos then
-        HoverInfo.inside (hoverPos - headPos).byteIdx
-      else
-        HoverInfo.after
-    let ⟨headPosLine, _⟩ := fileMap.toPosition headPos
-    let ⟨tailPosLine, _⟩ := fileMap.toPosition info.tailPos?.get!
-    if headPosLine != hoverLine || headPosLine != tailPosLine then
-      return best
-    return best.push { hoverInfo, ctx, info := completionInfo }
-
-private def computePrioritizedCompletionPartitions
-    (items : Array (ContextualizedCompletionInfo × Nat))
-    : Array (Array (ContextualizedCompletionInfo × Nat)) :=
-  let partitions := items.groupByKey fun (i, _) =>
-    let isId := i.info matches .id ..
-    let size? := Info.ofCompletionInfo i.info |>.size?
-    (isId, size?)
-  -- Sort partitions so that non-id completions infos come before id completion infos and
-  -- within those two groups, smaller sizes come before larger sizes.
-  let partitionsByPriority := partitions.toArray.qsort
-    fun ((isId₁, size₁?), _) ((isId₂, size₂?), _) =>
-      match size₁?, size₂? with
-      | some _, none   => true
-      | none,   some _ => false
-      | _, _ =>
-        match isId₁, isId₂ with
-        | false, true  => true
-        | true,  false => false
-        | _,     _     => Id.run do
-          let some size₁ := size₁?
-            | return false
-          let some size₂ := size₂?
-            | return false
-          return size₁ < size₂
-  partitionsByPriority.map (·.2)
-
-/--
-Finds all `CompletionInfo`s (both from the `InfoTree` and synthetic ones), prioritizes them,
-arranges them in partitions of `CompletionInfo`s with the same priority and sorts these partitions
-so that `CompletionInfo`s with the highest priority come first.
-The returned `CompletionInfo`s are also tagged with their index in `findCompletionInfosAt` so that
-when resolving a `CompletionItem`, we can reconstruct which `CompletionInfo` it was created from.
-
-In general, the `InfoTree` may contain multiple different `CompletionInfo`s covering `hoverPos`,
-and so we need to decide which of these `CompletionInfo`s we want to use to show completions to the
-user. We choose priorities by the following rules:
-- Synthetic completions have the lowest priority since they are only intended as a backup.
-- Non-identifier completions have the highest priority since they tend to be much more helpful than
-  identifier completions when available since there are typically way too many of the latter.
-- Within the three groups [non-id completions, id completions, synthetic completions],
-  `CompletionInfo`s with a smaller range are considered to be better.
--/
-def findPrioritizedCompletionPartitionsAt
-    (fileMap  : FileMap)
-    (hoverPos : String.Pos)
-    (cmdStx   : Syntax)
-    (infoTree : InfoTree)
-    : Array (Array (ContextualizedCompletionInfo × Nat)) :=
-  findCompletionInfosAt fileMap hoverPos cmdStx infoTree
-    |>.zipWithIndex
-    |> computePrioritizedCompletionPartitions
-
-end Lean.Server.Completion

src/Lean/Server/Completion/CompletionResolution.lean

@@ -1,91 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Marc Huisinga
--/
-prelude
-import Lean.Server.Completion.CompletionItemData
-import Lean.Server.Completion.CompletionInfoSelection
-
-namespace Lean.Lsp
-
-/--
-Identifier that is sent from the server to the client as part of the `CompletionItem.data?` field.
-Needed to resolve the `CompletionItem` when the client sends a `completionItem/resolve` request
-for that item, again containing the `data?` field provided by the server.
--/
-inductive CompletionIdentifier where
-  | const (declName : Name)
-  | fvar  (id       : FVarId)
-  deriving FromJson, ToJson
-
-/--
-`CompletionItemData` that contains additional information to identify the item
-in order to resolve it.
--/
-structure ResolvableCompletionItemData extends CompletionItemData where
-  /-- Position of the completion info that this completion item was created from. -/
-  cPos : Nat
-  id?  : Option CompletionIdentifier
-  deriving FromJson, ToJson
-
-private partial def consumeImplicitPrefix (e : Expr) (k : Expr → MetaM α) : MetaM α := do
-  match e with
-  | Expr.forallE n d b c =>
-    -- We do not consume instance implicit arguments because the user probably wants be aware of this dependency
-    if c == .implicit then
-      Meta.withLocalDecl n c d fun arg =>
-        consumeImplicitPrefix (b.instantiate1 arg) k
-    else
-      k e
-  | _ => k e
-
-/--
-Fills the `CompletionItem.detail?` field of `item` using the pretty-printed type identified by `id`.
--/
-def CompletionItem.resolve
-    (item : CompletionItem)
-    (id   : CompletionIdentifier)
-    : MetaM CompletionItem := do
-  let env ← getEnv
-  let lctx ← getLCtx
-  let mut item := item
-
-  if item.detail?.isNone then
-    let type? := match id with
-      | .const declName =>
-        env.find? declName |>.map ConstantInfo.type
-      | .fvar id =>
-        lctx.find? id |>.map LocalDecl.type
-    let detail? ← type?.mapM fun type =>
-      consumeImplicitPrefix type fun typeWithoutImplicits =>
-        return toString (← Meta.ppExpr typeWithoutImplicits)
-    item := { item with detail? := detail? }
-
-  return item
-
-end Lean.Lsp
-
-namespace Lean.Server.Completion
-open Lean.Lsp
-open Elab
-
-/--
-Fills the `CompletionItem.detail?` field of `item` using the pretty-printed type identified by `id`
-in the context found at `hoverPos` in `infoTree`.
--/
-def resolveCompletionItem?
-    (fileMap           : FileMap)
-    (hoverPos          : String.Pos)
-    (cmdStx            : Syntax)
-    (infoTree          : InfoTree)
-    (item              : CompletionItem)
-    (id                : CompletionIdentifier)
-    (completionInfoPos : Nat)
-    : IO CompletionItem := do
-  let completionInfos := findCompletionInfosAt fileMap hoverPos cmdStx infoTree
-  let some i := completionInfos.get? completionInfoPos
-    | return item
-  i.ctx.runMetaM i.info.lctx (item.resolve id)
-
-end Lean.Server.Completion

src/Lean/Server/Completion/CompletionUtils.lean

@@ -1,22 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Marc Huisinga
--/
-prelude
-import Init.Prelude
-import Lean.Elab.InfoTree.Types
-
-namespace Lean.Server.Completion
-open Elab
-
-inductive HoverInfo : Type where
-  | after
-  | inside (delta : Nat)
-
-structure ContextualizedCompletionInfo where
-  hoverInfo : HoverInfo
-  ctx       : ContextInfo
-  info      : CompletionInfo
-
-end Lean.Server.Completion

src/Lean/Server/Completion/EligibleHeaderDecls.lean

@@ -1,53 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Marc Huisinga
--/
-prelude
-import Lean.Meta.CompletionName
-
-namespace Lean.Server.Completion
-open Meta
-
-abbrev EligibleHeaderDecls := Std.HashMap Name ConstantInfo
-
-/-- Cached header declarations for which `allowCompletion headerEnv decl` is true. -/
-builtin_initialize eligibleHeaderDeclsRef : IO.Ref (Option EligibleHeaderDecls) ←
-  IO.mkRef none
-
-/--
-Returns the declarations in the header for which `allowCompletion env decl` is true, caching them
-if not already cached.
--/
-def getEligibleHeaderDecls (env : Environment) : IO EligibleHeaderDecls := do
-  eligibleHeaderDeclsRef.modifyGet fun
-    | some eligibleHeaderDecls => (eligibleHeaderDecls, some eligibleHeaderDecls)
-    | none =>
-      let (_, eligibleHeaderDecls) :=
-        StateT.run (m := Id) (s := {}) do
-          -- `map₁` are the header decls
-          env.constants.map₁.forM fun declName c => do
-            modify fun eligibleHeaderDecls =>
-              if allowCompletion env declName then
-                eligibleHeaderDecls.insert declName c
-              else
-                eligibleHeaderDecls
-      (eligibleHeaderDecls, some eligibleHeaderDecls)
-
-/-- Iterate over all declarations that are allowed in completion results. -/
-def forEligibleDeclsM [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m]
-    [MonadLiftT IO m] (f : Name → ConstantInfo → m PUnit) : m PUnit := do
-  let env ← getEnv
-  (← getEligibleHeaderDecls env).forM f
-  -- map₂ are exactly the local decls
-  env.constants.map₂.forM fun name c => do
-    if allowCompletion env name then
-      f name c
-
-/-- Checks whether this declaration can appear in completion results. -/
-def allowCompletion (eligibleHeaderDecls : EligibleHeaderDecls) (env : Environment)
-    (declName : Name) : Bool :=
-  eligibleHeaderDecls.contains declName ||
-    env.constants.map₂.contains declName && Lean.Meta.allowCompletion env declName
-
-end Lean.Server.Completion

src/Lean/Server/Completion/SyntheticCompletion.lean

@@ -1,396 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Marc Huisinga
--/
-prelude
-import Lean.Server.InfoUtils
-import Lean.Server.Completion.CompletionUtils
-
-namespace Lean.Server.Completion
-open Elab
-
-private def findBest?
-    (infoTree : InfoTree)
-    (gt : α → α → Bool)
-    (f : ContextInfo → Info → PersistentArray InfoTree → Option α)
-    : Option α :=
-  infoTree.visitM (m := Id) (postNode := choose) |>.join
-where
-  choose
-      (ctx : ContextInfo)
-      (info : Info)
-      (cs : PersistentArray InfoTree)
-      (childValues : List (Option (Option α)))
-      : Option α :=
-    let bestChildValue := childValues.map (·.join) |>.foldl (init := none) fun v best =>
-      if isBetter v best then
-        v
-      else
-        best
-    if let some v := f ctx info cs then
-      if isBetter v bestChildValue then
-        v
-      else
-        bestChildValue
-    else
-      bestChildValue
-  isBetter (a b : Option α) : Bool :=
-    match a, b with
-    | none,   none   => false
-    | some _, none   => true
-    | none,   some _ => false
-    | some a, some b => gt a b
-
-/--
-If there are `Info`s that contain `hoverPos` and have a nonempty `LocalContext`,
-yields the closest one of those `Info`s.
-Otherwise, yields the closest `Info` that contains `hoverPos` and has an empty `LocalContext`.
--/
-private def findClosestInfoWithLocalContextAt?
-    (hoverPos : String.Pos)
-    (infoTree : InfoTree)
-    : Option (ContextInfo × Info) :=
-  findBest? infoTree isBetter fun ctx info _ =>
-    if info.occursInOrOnBoundary hoverPos then
-      (ctx, info)
-    else
-      none
-where
-  isBetter (a b : ContextInfo × Info) : Bool :=
-    let (_, ia) := a
-    let (_, ib) := b
-    if !ia.lctx.isEmpty && ib.lctx.isEmpty then
-      true
-    else if ia.lctx.isEmpty && !ib.lctx.isEmpty then
-      false
-    else if ia.isSmaller ib then
-      true
-    else if ib.isSmaller ia then
-      false
-    else
-      false
-
-private def findSyntheticIdentifierCompletion?
-    (hoverPos : String.Pos)
-    (infoTree : InfoTree)
-    : Option ContextualizedCompletionInfo := do
-  let some (ctx, info) := findClosestInfoWithLocalContextAt? hoverPos infoTree
-    | none
-  let some stack := info.stx.findStack? (·.getRange?.any (·.contains hoverPos (includeStop := true)))
-    | none
-  let stack := stack.dropWhile fun (stx, _) => !(stx matches `($_:ident) || stx matches `($_:ident.))
-  let some (stx, _) := stack.head?
-    | none
-  let isDotIdCompletion := stack.any fun (stx, _) => stx matches `(.$_:ident)
-  if isDotIdCompletion then
-    -- An identifier completion is never useful in a dotId completion context.
-    none
-  let some (id, danglingDot) :=
-      match stx with
-      | `($id:ident) => some (id.getId, false)
-      | `($id:ident.) => some (id.getId, true)
-      | _ => none
-    | none
-  let tailPos := stx.getTailPos?.get!
-  let hoverInfo :=
-    if hoverPos < tailPos then
-      HoverInfo.inside (tailPos - hoverPos).byteIdx
-    else
-      HoverInfo.after
-  some { hoverInfo, ctx, info := .id stx id danglingDot info.lctx none }
-
-private partial def getIndentationAmount (fileMap : FileMap) (line : Nat) : Nat := Id.run do
-  let lineStartPos := fileMap.lineStart line
-  let lineEndPos := fileMap.lineStart (line + 1)
-  let mut it : String.Iterator := ⟨fileMap.source, lineStartPos⟩
-  let mut indentationAmount := 0
-  while it.pos < lineEndPos do
-    let c := it.curr
-    if c = ' ' || c = '\t' then
-      indentationAmount := indentationAmount + 1
-    else
-      break
-    it := it.next
-  return indentationAmount
-
-private partial def isCursorOnWhitespace (fileMap : FileMap) (hoverPos : String.Pos) : Bool :=
-  fileMap.source.atEnd hoverPos || (fileMap.source.get hoverPos).isWhitespace
-
-private partial def isCursorInProperWhitespace (fileMap : FileMap) (hoverPos : String.Pos) : Bool :=
-  (fileMap.source.atEnd hoverPos || (fileMap.source.get hoverPos).isWhitespace)
-    && (fileMap.source.get (hoverPos - ⟨1⟩)).isWhitespace
-
-private partial def isSyntheticTacticCompletion
-    (fileMap  : FileMap)
-    (hoverPos : String.Pos)
-    (cmdStx   : Syntax)
-    : Bool := Id.run do
-  let hoverFilePos := fileMap.toPosition hoverPos
-  let mut hoverLineIndentation := getIndentationAmount fileMap hoverFilePos.line
-  if hoverFilePos.column < hoverLineIndentation then
-    -- Ignore trailing whitespace after the cursor
-    hoverLineIndentation := hoverFilePos.column
-  go hoverFilePos hoverLineIndentation cmdStx 0
-where
-  go
-      (hoverFilePos : Position)
-      (hoverLineIndentation : Nat)
-      (stx : Syntax)
-      (leadingWs : Nat)
-      : Bool := Id.run do
-    match stx.getPos?, stx.getTailPos? with
-    | some startPos, some endPos =>
-      let isCursorInCompletionRange :=
-        startPos.byteIdx - leadingWs <= hoverPos.byteIdx
-          && hoverPos.byteIdx <= endPos.byteIdx + stx.getTrailingSize
-      if ! isCursorInCompletionRange then
-        return false
-      let mut wsBeforeArg := leadingWs
-      for arg in stx.getArgs do
-        if go hoverFilePos hoverLineIndentation arg wsBeforeArg then
-          return true
-        -- We must account for the whitespace before an argument because the syntax nodes we use
-        -- to identify tactic blocks only start *after* the whitespace following a `by`, and we
-        -- want to provide tactic completions in that whitespace as well.
-        -- This method of computing whitespace assumes that there are no syntax nodes without tokens
-        -- after `by` and before the first proper tactic syntax.
-        wsBeforeArg := arg.getTrailingSize
-      return isCompletionInEmptyTacticBlock stx
-        || isCompletionAfterSemicolon stx
-        || isCompletionOnTacticBlockIndentation hoverFilePos hoverLineIndentation stx
-    | _, _ =>
-      -- Empty tactic blocks typically lack ranges since they do not contain any tokens.
-      -- We do not perform more precise range checking in this case because we assume that empty
-      -- tactic blocks always occur within other syntax with ranges that let us narrow down the
-      -- search to the degree that we can be sure that the cursor is indeed in this empty tactic
-      -- block.
-      return isCompletionInEmptyTacticBlock stx
-
-  isCompletionOnTacticBlockIndentation
-      (hoverFilePos : Position)
-      (hoverLineIndentation : Nat)
-      (stx : Syntax)
-      : Bool := Id.run do
-    let isCursorInIndentation := hoverFilePos.column <= hoverLineIndentation
-    if ! isCursorInIndentation then
-      -- Do not trigger tactic completion at the end of a properly indented tactic block line since
-      -- that line might already have entered term mode by that point.
-      return false
-    let some tacticsNode := getTacticsNode? stx
-      | return false
-    let some firstTacticPos := tacticsNode.getPos?
-      | return false
-    let firstTacticLine := fileMap.toPosition firstTacticPos |>.line
-    let firstTacticIndentation := getIndentationAmount fileMap firstTacticLine
-    -- This ensures that we do not accidentally provide tactic completions in a term mode proof -
-    -- tactic completions are only provided at the same indentation level as the other tactics in
-    -- that tactic block.
-    let isCursorInTacticBlock := hoverLineIndentation == firstTacticIndentation
-    return isCursorInProperWhitespace fileMap hoverPos && isCursorInTacticBlock
-
-  isCompletionAfterSemicolon (stx : Syntax) : Bool := Id.run do
-    let some tacticsNode := getTacticsNode? stx
-      | return false
-    let tactics := tacticsNode.getArgs
-    -- We want to provide completions in the case of `skip;<CURSOR>`, so the cursor must only be on
-    -- whitespace, not in proper whitespace.
-    return isCursorOnWhitespace fileMap hoverPos && tactics.any fun tactic => Id.run do
-      let some tailPos := tactic.getTailPos?
-        | return false
-      let isCursorAfterSemicolon :=
-        tactic.isToken ";"
-          && tailPos.byteIdx <= hoverPos.byteIdx
-          && hoverPos.byteIdx <= tailPos.byteIdx + tactic.getTrailingSize
-      return isCursorAfterSemicolon
-
-  getTacticsNode? (stx : Syntax) : Option Syntax :=
-    if stx.getKind == ``Parser.Tactic.tacticSeq1Indented then
-      some stx[0]
-    else if stx.getKind == ``Parser.Tactic.tacticSeqBracketed then
-      some stx[1]
-    else
-      none
-
-  isCompletionInEmptyTacticBlock (stx : Syntax) : Bool :=
-    isCursorInProperWhitespace fileMap hoverPos && isEmptyTacticBlock stx
-
-  isEmptyTacticBlock (stx : Syntax) : Bool :=
-    stx.getKind == ``Parser.Tactic.tacticSeq && isEmpty stx
-      || stx.getKind == ``Parser.Tactic.tacticSeq1Indented && isEmpty stx
-      || stx.getKind == ``Parser.Tactic.tacticSeqBracketed && isEmpty stx[1]
-
-  isEmpty : Syntax → Bool
-    | .missing       => true
-    | .ident ..      => false
-    | .atom ..       => false
-    | .node _ _ args => args.all isEmpty
-
-private partial def findOutermostContextInfo? (i : InfoTree) : Option ContextInfo :=
-  go i
-where
-  go (i : InfoTree) : Option ContextInfo := do
-    match i with
-  | .context ctx i =>
-    match ctx with
-    | .commandCtx ctxInfo =>
-      some { ctxInfo with }
-    | _ =>
-      -- This shouldn't happen (see the `PartialContextInfo` docstring),
-      -- but let's continue searching regardless
-      go i
-  | .node _ cs =>
-    cs.findSome? go
-  | .hole .. =>
-    none
-
-private def findSyntheticTacticCompletion?
-    (fileMap  : FileMap)
-    (hoverPos : String.Pos)
-    (cmdStx   : Syntax)
-    (infoTree : InfoTree)
-    : Option ContextualizedCompletionInfo := do
-  let ctx ← findOutermostContextInfo? infoTree
-  if ! isSyntheticTacticCompletion fileMap hoverPos cmdStx then
-    none
-  -- Neither `HoverInfo` nor the syntax in `.tactic` are important for tactic completion.
-  return { hoverInfo := HoverInfo.after, ctx, info := .tactic .missing }
-
-private def findExpectedTypeAt (infoTree : InfoTree) (hoverPos : String.Pos) : Option (ContextInfo × Expr) := do
-  let (ctx, .ofTermInfo i) ← infoTree.smallestInfo? fun i => Id.run do
-      let some pos := i.pos?
-        | return false
-      let some tailPos := i.tailPos?
-        | return false
-      let .ofTermInfo ti := i
-        | return false
-      return ti.expectedType?.isSome && pos <= hoverPos && hoverPos <= tailPos
-    | none
-  (ctx, i.expectedType?.get!)
-
-private partial def foldWithLeadingToken [Inhabited α]
-    (f    : α → Option Syntax → Syntax → α)
-    (init : α)
-    (stx  : Syntax)
-    : α :=
-  let (_, r) := go none init stx
-  r
-where
-  go [Inhabited α] (leadingToken? : Option Syntax) (acc : α) (stx : Syntax) : Option Syntax × α :=
-    let acc := f acc leadingToken? stx
-    match stx with
-    | .missing  => (none, acc)
-    | .atom ..  => (stx, acc)
-    | .ident .. => (stx, acc)
-    | .node _ _ args => Id.run do
-      let mut acc := acc
-      let mut lastToken? := none
-      for arg in args do
-        let (lastToken'?, acc') := go (lastToken? <|> leadingToken?) acc arg
-        lastToken? := lastToken'? <|> lastToken?
-        acc := acc'
-      return (lastToken?, acc)
-
-private def findWithLeadingToken?
-    (p : Option Syntax → Syntax → Bool)
-    (stx : Syntax)
-    : Option Syntax :=
-  foldWithLeadingToken (stx := stx) (init := none) fun foundStx? leadingToken? stx =>
-    match foundStx? with
-    | some foundStx => foundStx
-    | none =>
-      if p leadingToken? stx then
-        some stx
-      else
-        none
-
-private def isSyntheticStructFieldCompletion
-    (fileMap  : FileMap)
-    (hoverPos : String.Pos)
-    (cmdStx   : Syntax)
-    : Bool := Id.run do
-  let isCursorOnWhitespace := isCursorOnWhitespace fileMap hoverPos
-  let isCursorInProperWhitespace := isCursorInProperWhitespace fileMap hoverPos
-  if ! isCursorOnWhitespace then
-    return false
-
-  let hoverFilePos := fileMap.toPosition hoverPos
-  let mut hoverLineIndentation := getIndentationAmount fileMap hoverFilePos.line
-  if hoverFilePos.column < hoverLineIndentation then
-    -- Ignore trailing whitespace after the cursor
-    hoverLineIndentation := hoverFilePos.column
-
-  return Option.isSome <| findWithLeadingToken? (stx := cmdStx) fun leadingToken? stx => Id.run do
-    let some leadingToken := leadingToken?
-      | return false
-
-    if stx.getKind != ``Parser.Term.structInstFields then
-      return false
-
-    let fieldsAndSeps := stx[0].getArgs
-    let some outerBoundsStart := leadingToken.getTailPos? (canonicalOnly := true)
-      | return false
-    let some outerBoundsStop :=
-        stx.getTrailingTailPos? (canonicalOnly := true)
-          <|> leadingToken.getTrailingTailPos? (canonicalOnly := true)
-      | return false
-    let outerBounds : String.Range := ⟨outerBoundsStart, outerBoundsStop⟩
-
-    let isCompletionInEmptyBlock :=
-      fieldsAndSeps.isEmpty && outerBounds.contains hoverPos (includeStop := true)
-    if isCompletionInEmptyBlock then
-      return true
-
-    let isCompletionAfterSep := fieldsAndSeps.zipWithIndex.any fun (fieldOrSep, i) => Id.run do
-      if i % 2 == 0 || !fieldOrSep.isAtom then
-        return false
-      let sep := fieldOrSep
-      let some sepTailPos := sep.getTailPos?
-        | return false
-      return sepTailPos <= hoverPos
-        && hoverPos.byteIdx <= sepTailPos.byteIdx + sep.getTrailingSize
-    if isCompletionAfterSep then
-      return true
-
-    let isCompletionOnIndentation := Id.run do
-      if ! isCursorInProperWhitespace then
-        return false
-      let isCursorInIndentation := hoverFilePos.column <= hoverLineIndentation
-      if ! isCursorInIndentation then
-        return false
-      let some firstFieldPos := stx.getPos?
-        | return false
-      let firstFieldLine := fileMap.toPosition firstFieldPos |>.line
-      let firstFieldIndentation := getIndentationAmount fileMap firstFieldLine
-      let isCursorInBlock := hoverLineIndentation == firstFieldIndentation
-      return isCursorInBlock
-    return isCompletionOnIndentation
-
-private def findSyntheticFieldCompletion?
-  (fileMap  : FileMap)
-  (hoverPos : String.Pos)
-  (cmdStx   : Syntax)
-  (infoTree : InfoTree)
-  : Option ContextualizedCompletionInfo := do
-  if ! isSyntheticStructFieldCompletion fileMap hoverPos cmdStx then
-    none
-  let (ctx, expectedType) ← findExpectedTypeAt infoTree hoverPos
-  let .const typeName _ := expectedType.getAppFn
-    | none
-  if ! isStructure ctx.env typeName then
-    none
-  return { hoverInfo := HoverInfo.after, ctx, info := .fieldId .missing none .empty typeName }
-
-def findSyntheticCompletions
-    (fileMap  : FileMap)
-    (hoverPos : String.Pos)
-    (cmdStx   : Syntax)
-    (infoTree : InfoTree)
-    : Array ContextualizedCompletionInfo :=
-  let syntheticCompletionData? : Option ContextualizedCompletionInfo :=
-    findSyntheticTacticCompletion? fileMap hoverPos cmdStx infoTree <|>
-      findSyntheticFieldCompletion? fileMap hoverPos cmdStx infoTree <|>
-        findSyntheticIdentifierCompletion? hoverPos infoTree
-  syntheticCompletionData?.map (#[·]) |>.getD #[]
-
-end Lean.Server.Completion

src/Lean/Server/FileWorker.lean

@@ -28,7 +28,7 @@ import Lean.Server.FileWorker.WidgetRequests
 import Lean.Server.FileWorker.SetupFile
 import Lean.Server.Rpc.Basic
 import Lean.Widget.InteractiveDiagnostic
-import Lean.Server.Completion.ImportCompletion
+import Lean.Server.ImportCompletion
 
 /-!
 For general server architecture, see `README.md`. For details of IPC communication, see `Watchdog.lean`.

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -33,9 +33,9 @@ def findCompletionCmdDataAtPos
     (pos : String.Pos)
     : Task (Option (Syntax × Elab.InfoTree)) :=
   findCmdDataAtPos doc (pos := pos) fun s => Id.run do
-    let some tailPos := s.stx.getTailPos?
+    let some tailPos := s.data.stx.getTailPos?
       | return false
-    return pos.byteIdx <= tailPos.byteIdx + s.stx.getTrailingSize
+    return pos.byteIdx <= tailPos.byteIdx + s.data.stx.getTrailingSize
 
 def handleCompletion (p : CompletionParams)
     : RequestM (RequestTask CompletionList) := do
@@ -46,11 +46,10 @@ def handleCompletion (p : CompletionParams)
   mapTask (findCompletionCmdDataAtPos doc pos) fun cmdData? => do
     let some (cmdStx, infoTree) := cmdData?
       -- work around https://github.com/microsoft/vscode/issues/155738
-      | return {
-        items := #[{label := "-", data? := toJson { params := p : Lean.Lsp.CompletionItemData }}],
-        isIncomplete := true
-      }
-    Completion.find? p doc.meta.text pos cmdStx infoTree caps
+      | return { items := #[{label := "-"}], isIncomplete := true }
+    if let some r ← Completion.find? p doc.meta.text pos cmdStx infoTree caps then
+      return r
+    return { items := #[ ], isIncomplete := true }
 
 /--
 Handles `completionItem/resolve` requests that are sent by the client after the user selects
@@ -63,7 +62,7 @@ def handleCompletionItemResolve (item : CompletionItem)
     : RequestM (RequestTask CompletionItem) := do
   let doc ← readDoc
   let text := doc.meta.text
-  let some (data : ResolvableCompletionItemData) := item.data?.bind fun data => (fromJson? data).toOption
+  let some (data : CompletionItemDataWithId) := item.data?.bind fun data => (fromJson? data).toOption
     | return .pure item
   let some id := data.id?
     | return .pure item
@@ -71,7 +70,7 @@ def handleCompletionItemResolve (item : CompletionItem)
   mapTask (findCompletionCmdDataAtPos doc pos) fun cmdData? => do
     let some (cmdStx, infoTree) := cmdData?
       | return item
-    Completion.resolveCompletionItem? text pos cmdStx infoTree item id data.cPos
+    Completion.resolveCompletionItem? text pos cmdStx infoTree item id
 
 open Elab in
 def handleHover (p : HoverParams)

src/Lean/Server/FileWorker/Utils.lean

@@ -28,10 +28,10 @@ private partial def mkCmdSnaps (initSnap : Language.Lean.InitialSnapshot) :
     } <| .delayed <| headerSuccess.firstCmdSnap.task.bind go
 where
   go cmdParsed :=
-    cmdParsed.finishedSnap.task.map fun finished =>
+    cmdParsed.data.finishedSnap.task.map fun finished =>
       .ok <| .cons {
-        stx := cmdParsed.stx
-        mpState := cmdParsed.parserState
+        stx := cmdParsed.data.stx
+        mpState := cmdParsed.data.parserState
         cmdState := finished.cmdState
       } (match cmdParsed.nextCmdSnap? with
         | some next => .delayed <| next.task.bind go

src/Lean/Server/ImportCompletion.lean

@@ -4,10 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Marc Huisinga
 -/
 prelude
+import Lean.Data.Name
 import Lean.Data.NameTrie
+import Lean.Data.Lsp.Utf16
+import Lean.Data.Lsp.LanguageFeatures
 import Lean.Util.Paths
 import Lean.Util.LakePath
-import Lean.Server.Completion.CompletionItemData
+import Lean.Server.CompletionItemData
 
 namespace ImportCompletion
 

src/Lean/Server/InfoUtils.lean

@@ -136,7 +136,6 @@ def InfoTree.getCompletionInfos (infoTree : InfoTree) : Array (ContextInfo × Co
 def Info.stx : Info → Syntax
   | ofTacticInfo i         => i.stx
   | ofTermInfo i           => i.stx
-  | ofPartialTermInfo i    => i.stx
   | ofCommandInfo i        => i.stx
   | ofMacroExpansionInfo i => i.stx
   | ofOptionInfo i         => i.stx
@@ -147,7 +146,6 @@ def Info.stx : Info → Syntax
   | ofFVarAliasInfo _      => .missing
   | ofFieldRedeclInfo i    => i.stx
   | ofOmissionInfo i       => i.stx
-  | ofChoiceInfo i         => i.stx
 
 def Info.lctx : Info → LocalContext
   | .ofTermInfo i           => i.lctx

src/Lean/Server/Requests.lean

@@ -204,7 +204,7 @@ partial def findInfoTreeAtPos
   findCmdParsedSnap doc (isMatchingSnapshot ·) |>.bind (sync := true) fun
     | some cmdParsed => toSnapshotTree cmdParsed |>.findInfoTreeAtPos pos |>.bind (sync := true) fun
       | some infoTree => .pure <| some infoTree
-      | none          => cmdParsed.finishedSnap.task.map (sync := true) fun s =>
+      | none          => cmdParsed.data.finishedSnap.task.map (sync := true) fun s =>
         -- the parser returns exactly one command per snapshot, and the elaborator creates exactly one node per command
         assert! s.cmdState.infoState.trees.size == 1
         some s.cmdState.infoState.trees[0]!
@@ -225,11 +225,11 @@ def findCmdDataAtPos
     : Task (Option (Syntax × Elab.InfoTree)) :=
   findCmdParsedSnap doc (isMatchingSnapshot ·) |>.bind (sync := true) fun
     | some cmdParsed => toSnapshotTree cmdParsed |>.findInfoTreeAtPos pos |>.bind (sync := true) fun
-      | some infoTree => .pure <| some (cmdParsed.stx, infoTree)
-      | none          => cmdParsed.finishedSnap.task.map (sync := true) fun s =>
+      | some infoTree => .pure <| some (cmdParsed.data.stx, infoTree)
+      | none          => cmdParsed.data.finishedSnap.task.map (sync := true) fun s =>
         -- the parser returns exactly one command per snapshot, and the elaborator creates exactly one node per command
         assert! s.cmdState.infoState.trees.size == 1
-        some (cmdParsed.stx, s.cmdState.infoState.trees[0]!)
+        some (cmdParsed.data.stx, s.cmdState.infoState.trees[0]!)
     | none => .pure none
 
 /--
@@ -244,7 +244,7 @@ def findInfoTreeAtPosWithTrailingWhitespace
     : Task (Option Elab.InfoTree) :=
   -- NOTE: use `>=` since the cursor can be *after* the input (and there is no interesting info on
   -- the first character of the subsequent command if any)
-  findInfoTreeAtPos doc (·.parserState.pos ≥ pos) pos
+  findInfoTreeAtPos doc (·.data.parserState.pos ≥ pos) pos
 
 open Elab.Command in
 def runCommandElabM (snap : Snapshot) (c : RequestT CommandElabM α) : RequestM α := do

src/Lean/Structure.lean

@@ -383,7 +383,7 @@ partial def computeStructureResolutionOrder [Monad m] [MonadEnv m]
   -- `resOrders` contains the resolution orders to merge.
   -- The parent list is inserted as a pseudo resolution order to ensure immediate parents come out in order,
   -- and it is added first to be the primary ordering constraint when there are ordering errors.
-  let mut resOrders := parentResOrders.insertIdx 0 parentNames |>.filter (!·.isEmpty)
+  let mut resOrders := parentResOrders.insertAt 0 parentNames |>.filter (!·.isEmpty)
 
   let mut resOrder : Array Name := #[structName]
   let mut defects : Array StructureResolutionOrderConflict := #[]

src/Lean/Syntax.lean

@@ -248,11 +248,11 @@ partial def updateTrailing (trailing : Substring) : Syntax → Syntax
   | Syntax.atom info val               => Syntax.atom (info.updateTrailing trailing) val
   | Syntax.ident info rawVal val pre   => Syntax.ident (info.updateTrailing trailing) rawVal val pre
   | n@(Syntax.node info k args)        =>
-    if h : args.size = 0 then n
+    if args.size == 0 then n
     else
      let i    := args.size - 1
-     let last := updateTrailing trailing args[i]
-     let args := args.set i last;
+     let last := updateTrailing trailing args[i]!
+     let args := args.set! i last;
      Syntax.node info k args
   | s => s