deprecations

This PR improves the `#print` command for structures to show all fields
and which parents the fields were inherited from, hiding internal
details such as which parents are represented as subobjects. This
information is still present in the constructor if needed. The pretty
printer for private constants is also improved, and it now handles
private names from the current module like any other name; private names
from other modules are made hygienic.

Example output for `#print Monad`:
```
class Monad.{u, v} (m : Type u → Type v) : Type (max (u + 1) v)
number of parameters: 1
parents:
  Monad.toApplicative : Applicative m
  Monad.toBind : Bind m
fields:
  Functor.map : {α β : Type u} → (α → β) → m α → m β
  Functor.mapConst : {α β : Type u} → α → m β → m α
  Pure.pure : {α : Type u} → α → m α
  Seq.seq : {α β : Type u} → m (α → β) → (Unit → m α) → m β
  SeqLeft.seqLeft : {α β : Type u} → m α → (Unit → m β) → m α
  SeqRight.seqRight : {α β : Type u} → m α → (Unit → m β) → m β
  Bind.bind : {α β : Type u} → m α → (α → m β) → m β
constructor:
  Monad.mk.{u, v} {m : Type u → Type v} [toApplicative : Applicative m] [toBind : Bind m] : Monad m
resolution order:
  Monad, Applicative, Bind, Functor, Pure, Seq, SeqLeft, SeqRight
```

Suggested by Floris van Doorn [on
Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.23print.20command.20for.20structures/near/482503637).

src/Init/Data/Array/Attach.lean

@@ -10,12 +10,13 @@ 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
+We replace this at runtime with a more efficient version via the `csimp` lemma `pmap_eq_pmapImpl`.
 -/
 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
@@ -73,6 +74,17 @@ 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
@@ -80,6 +92,353 @@ 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`.
@@ -128,6 +487,15 @@ 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/Find.lean

@@ -272,4 +272,10 @@ 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,6 +23,9 @@ 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
@@ -36,12 +39,21 @@ 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
@@ -66,6 +78,35 @@ 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
@@ -93,9 +134,6 @@ 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
@@ -605,19 +643,6 @@ theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
 
 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,10 +684,6 @@ 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?]
 
@@ -672,6 +693,10 @@ 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]
@@ -1025,6 +1050,10 @@ 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]
@@ -1215,6 +1244,12 @@ 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]
 
@@ -1914,6 +1949,26 @@ 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
@@ -1928,6 +1983,12 @@ theorem array_array_induction (P : Array (Array α) → Prop) (h : ∀ (xss : Li
   | 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/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`. -/
-@[simp] def pmap {P : α → Prop} (f : ∀ a, P a → β) : ∀ l : List α, (H : ∀ a ∈ l, P a) → List β
+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,6 +46,11 @@ 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
@@ -148,7 +153,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} : length (pmap f l H) = length l := by
+theorem length_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : (pmap f l H).length = l.length := by
   induction l
   · rfl
   · simp only [*, pmap, length]
@@ -199,7 +204,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 (getElem?_mem H) := by
+    (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (mem_of_getElem? H) := by
   induction l generalizing n with
   | nil => simp
   | cons hd tl hl =>
@@ -215,7 +220,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 (get?_mem H) := by
+    get? (pmap f l h) n = Option.pmap f (get? l n) fun x H => h x (mem_of_get? H) := by
   simp only [get?_eq_getElem?]
   simp [getElem?_pmap, h]
 
@@ -238,18 +243,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 _ (get_mem l n (@length_pmap _ _ p f l h ▸ hn))) := by
+        (h _ (getElem_mem (@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 _ (getElem?_mem 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 : List α} {i : Nat} :
-    xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => getElem?_mem a) :=
+    xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => mem_of_getElem? a) :=
   getElem?_attachWith
 
 @[simp]
@@ -333,6 +338,7 @@ 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
@@ -348,6 +354,7 @@ 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
@@ -452,16 +459,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_of_mem_left ys h⟩) ++
-      ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_of_mem_right xs h⟩ := by
+    (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
   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_of_mem_left ys h)) ++
-      ys.attachWith P (fun a h => H a (mem_append_of_mem_right xs h)) := by
+    (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 only [attachWith, attach_append, map_pmap, pmap_append]
 
 @[simp] theorem pmap_reverse {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
@@ -598,6 +605,15 @@ 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_of_mem_left {a : α} {as : List α} (bs : List α) : a ∈ as → a ∈ as ++ bs := by
+theorem mem_append_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_of_mem_right {b : α} {bs : List α} (as : List α) : b ∈ bs → b ∈ as ++ bs := by
+theorem mem_append_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_of_mem_right _ (Mem.head ..)
+        exact mem_append_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_of_mem_right xs (mem_cons_self a _)
+  mem_append_right xs (mem_cons_self a _)
 
-theorem mem_append_cons_self : a ∈ xs ++ a :: ys := mem_append_of_mem_right _ (mem_cons_self _ _)
+theorem mem_append_cons_self : a ∈ xs ++ a :: ys := mem_append_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,16 +503,20 @@ 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 h, get l ⟨n, h⟩ ∈ l
-  | _ :: _, 0, _ => .head ..
-  | _ :: l, _+1, _ => .tail _ (get_mem l ..)
+theorem get_mem : ∀ (l : List α) n, get l n ∈ l
+  | _ :: _, ⟨0, _⟩ => .head ..
+  | _ :: l, ⟨_+1, _⟩ => .tail _ (get_mem l ..)
 
-theorem getElem?_mem {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l :=
+theorem mem_of_getElem? {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l :=
   let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..
 
-theorem get?_mem {l : List α} {n a} (e : l.get? n = some a) : a ∈ l :=
+@[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 :=
   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 ..⟩
 
@@ -1997,11 +2001,8 @@ 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
 
-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)
+@[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_iff_append {a : α} {l : List α} : a ∈ l ↔ ∃ s t : List α, l = s ++ a :: t :=
   ⟨append_of_mem, fun ⟨s, t, e⟩ => e ▸ by simp⟩
@@ -2415,7 +2416,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 (get_mem _ _ _)
+  eq_of_mem_replicate (getElem_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_of_mem_right l₁' m) (h₂.mem m)
+    exact fun x m => w x (mem_append_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_of_mem_left l₂' m) (h₁.mem m)
+    exact fun x m => w x (mem_append_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) : IO Unit :=
+def IO.setRandSeed (n : Nat) : BaseIO Unit :=
   IO.stdGenRef.set (mkStdGen n)
 
-def IO.rand (lo hi : Nat) : IO Nat := do
+def IO.rand (lo hi : Nat) : BaseIO Nat := do
   let gen ← IO.stdGenRef.get
   let (r, gen) := randNat gen lo hi
   IO.stdGenRef.set gen

src/Init/Meta.lean

@@ -374,6 +374,9 @@ 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
@@ -382,14 +385,39 @@ 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). -/

src/Init/Prelude.lean

@@ -3654,7 +3654,8 @@ namespace SourceInfo
 
 /--
 Gets the position information from a `SourceInfo`, if available.
-If `originalOnly` is true, then `.synthetic` syntax will also return `none`.
+If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false`
+will also return `none`.
 -/
 def getPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
   match info, canonicalOnly with
@@ -3665,7 +3666,8 @@ def getPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
 
 /--
 Gets the end position information from a `SourceInfo`, if available.
-If `originalOnly` is true, then `.synthetic` syntax will also return `none`.
+If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false`
+will also return `none`.
 -/
 def getTailPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
   match info, canonicalOnly with
@@ -3674,6 +3676,24 @@ 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
 
 /--
@@ -3972,7 +3992,6 @@ 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/Lean/Data/Lsp/Basic.lean

@@ -365,6 +365,7 @@ structure TextDocumentRegistrationOptions where
 
 inductive MarkupKind where
   | plaintext | markdown
+  deriving DecidableEq, Hashable
 
 instance : FromJson MarkupKind := ⟨fun
   | str "plaintext" => Except.ok MarkupKind.plaintext
@@ -378,7 +379,7 @@ instance : ToJson MarkupKind := ⟨fun
 structure MarkupContent where
   kind  : MarkupKind
   value : String
-  deriving ToJson, FromJson
+  deriving ToJson, FromJson, DecidableEq, Hashable
 
 /-- 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
+  deriving Inhabited, DecidableEq, Repr, Hashable
 
 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
+  deriving FromJson, ToJson, BEq, Hashable
 
 inductive CompletionItemTag where
   | deprecated
-  deriving Inhabited, DecidableEq, Repr
+  deriving Inhabited, DecidableEq, Repr, Hashable
 
 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
+  deriving FromJson, ToJson, Inhabited, BEq, Hashable
 
 structure CompletionList where
   isIncomplete : Bool

src/Lean/Elab/App.lean

@@ -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 (fullRef := fullRef) .. := lval then
-      addDotCompletionInfo fullRef f expectedType?
+    if let LVal.fieldName (ref := ref) .. := lval then
+      addDotCompletionInfo ref f expectedType?
     let hasArgs := !namedArgs.isEmpty || !args.isEmpty
     let (f, lvalRes) ← resolveLVal f lval hasArgs
     match lvalRes with
@@ -1650,6 +1650,14 @@ 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/BuiltinTerm.lean

@@ -42,16 +42,15 @@ 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
-    /- 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. -/
+    -- 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?
     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?
@@ -328,7 +327,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) =>
-    withInfoContext' stx (elabTerm e expectedType?) (mkTermInfo .anonymous (expectedType? := expectedType?) stx)
+    withTermInfoContext' .anonymous stx (expectedType? := expectedType?) (elabTerm e expectedType?)
   | _ => throwUnsupportedSyntax
 
 private unsafe def evalFilePathUnsafe (stx : Syntax) : TermElabM System.FilePath :=

src/Lean/Elab/Command.lean

@@ -555,7 +555,11 @@ private def getVarDecls (s : State) : Array Syntax :=
 instance {α} : Inhabited (CommandElabM α) where
   default := throw default
 
-private def mkMetaContext : Meta.Context := {
+/--
+The environment linter framework needs to be able to run linters with the same context
+as `liftTermElabM`, so we expose that context as a public function here.
+-/
+def mkMetaContext : Meta.Context := {
   config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true }
 }
 

src/Lean/Elab/Extra.lean

@@ -327,15 +327,18 @@ 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 <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) do
-      mkBinOp (kind == .lazy) f (← toExprCore lhs) (← toExprCore rhs)
+    withRef ref <|
+      withTermInfoContext' .anonymous ref do
+        mkBinOp (kind == .lazy) f (← toExprCore lhs) (← toExprCore rhs)
   | .unop ref f arg =>
-    withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) do
-      mkUnOp f (← toExprCore arg)
+    withRef ref <|
+      withTermInfoContext' .anonymous ref do
+        mkUnOp f (← toExprCore arg)
   | .macroExpansion macroName stx stx' nested =>
-    withRef stx <| withInfoContext' stx (mkInfo := mkTermInfo macroName stx) do
-      withMacroExpansion stx stx' do
-        toExprCore nested
+    withRef stx <|
+      withTermInfoContext' macroName stx <|
+        withMacroExpansion stx stx' <|
+          toExprCore nested
 
 /--
   Auxiliary function to decide whether we should coerce `f`'s argument to `maxType` or not.

src/Lean/Elab/InfoTree/Main.lean

@@ -139,12 +139,16 @@ 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?}"
@@ -191,9 +195,13 @@ 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
@@ -204,10 +212,12 @@ 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
@@ -218,6 +228,7 @@ 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.
@@ -311,24 +322,36 @@ def realizeGlobalNameWithInfos (ref : Syntax) (id : Name) : CoreM (List (Name ×
       addConstInfo ref n
   return ns
 
-/-- Use this to descend a node on the infotree that is being built.
+/--
+Adds a node containing the `InfoTree`s generated by `x` to the `InfoTree`s in `m`.
 
-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 `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
   if (← getInfoState).enabled then
     let treesSaved ← getResetInfoTrees
     Prod.fst <$> MonadFinally.tryFinally' x fun a? => do
-      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
+      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
   else
     x
 

src/Lean/Elab/InfoTree/Types.lean

@@ -70,6 +70,18 @@ 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
 
@@ -79,7 +91,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 : Name) (lctx : LocalContext) (structName : Name)
+  | fieldId (stx : Syntax) (id : Option Name) (lctx : LocalContext) (structName : Name)
   | namespaceId (stx : Syntax)
   | option (stx : Syntax)
   | endSection (stx : Syntax) (scopeNames : List String)
@@ -165,10 +177,18 @@ 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)
@@ -179,6 +199,7 @@ 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

@@ -90,9 +90,12 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
       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 ·)) do
-          let value ← elabTermEnsuringType view.valStx type
-          mkLambdaFVars xs value
+        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
 
 private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array Expr) (values : Array Expr) : TermElabM Unit := do
   let letRecsToLiftCurr := (← get).letRecsToLift

src/Lean/Elab/Match.lean

@@ -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) fun p => do
+        Elab.withInfoContext' (go p) (mkInfoOnError := mkPartialTermInfo .anonymous stx) 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
-  | `(Parser.Command.whereStructInst|where $[$decls:letDecl];* $[$whereDecls?:whereDecls]?) => do
+  | whereStx@`(Parser.Command.whereStructInst|where%$whereTk $[$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,7 +300,30 @@ 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
@@ -417,12 +440,15 @@ 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 ·)) 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 ·))
+            (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
         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/PreDefinition/Structural/FindRecArg.lean

@@ -243,7 +243,7 @@ def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
     recArgInfoss := recArgInfoss.push recArgInfos
   -- Put non-indices first
   recArgInfoss := recArgInfoss.map nonIndicesFirst
-  trace[Elab.definition.structural] "recArgInfoss: {recArgInfoss.map (·.map (·.recArgPos))}"
+  trace[Elab.definition.structural] "recArgInfos:{indentD (.joinSep (recArgInfoss.flatten.toList.map (repr ·)) Format.line)}"
   -- Inductive groups to consider
   let groups ← inductiveGroups recArgInfoss.flatten
   trace[Elab.definition.structural] "inductive groups: {groups}"

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

@@ -27,7 +27,7 @@ constituents.
 structure IndGroupInfo where
   all       : Array Name
   numNested : Nat
-deriving BEq, Inhabited
+deriving BEq, Inhabited, Repr
 
 def IndGroupInfo.ofInductiveVal (indInfo : InductiveVal) : IndGroupInfo where
   all       := indInfo.all.toArray
@@ -56,7 +56,7 @@ mutual structural recursion on such incompatible types.
 structure IndGroupInst extends IndGroupInfo where
   levels    : List Level
   params    : Array Expr
-deriving Inhabited
+deriving Inhabited, Repr
 
 def IndGroupInst.toMessageData (igi : IndGroupInst) : MessageData :=
   mkAppN (.const igi.all[0]! igi.levels) igi.params

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

@@ -23,9 +23,9 @@ structure RecArgInfo where
   fnName       : Name
   /-- the fixed prefix of arguments of the function we are trying to justify termination using structural recursion. -/
   numFixed     : Nat
-  /-- position of the argument (counted including fixed prefix) we are recursing on -/
+  /-- position (counted including fixed prefix) of the argument we are recursing on -/
   recArgPos    : Nat
-  /-- position of the indices (counted including fixed prefix) of the inductive datatype indices we are recursing on -/
+  /-- position (counted including fixed prefix) of the indices of the inductive datatype we are recursing on -/
   indicesPos   : Array Nat
   /-- The inductive group (with parameters) of the argument's type -/
   indGroupInst : IndGroupInst
@@ -34,20 +34,23 @@ structure RecArgInfo where
   If `< indAll.all`, a normal data type, else an auxiliary data type due to nested recursion
   -/
   indIdx       : Nat
-deriving Inhabited
+deriving Inhabited, Repr
 
 /--
 If `xs` are the parameters of the functions (excluding fixed prefix), partitions them
 into indices and major arguments, and other parameters.
 -/
 def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array Expr × Array Expr) := Id.run do
+  -- First indices and major arg, using the order they appear in `info.indicesPos`
   let mut indexMajorArgs := #[]
+  let indexMajorPos := info.indicesPos.push info.recArgPos
+  for j in indexMajorPos do
+    assert! info.numFixed ≤ j && j - info.numFixed < xs.size
+    indexMajorArgs := indexMajorArgs.push xs[j - info.numFixed]!
+  -- Then the other arguments, in the order they appear in `xs`
   let mut otherArgs := #[]
   for h : i in [:xs.size] do
-    let j := i + info.numFixed
-    if j = info.recArgPos || info.indicesPos.contains j then
-      indexMajorArgs := indexMajorArgs.push xs[i]
-    else
+    unless indexMajorPos.contains (i + info.numFixed) do
       otherArgs := otherArgs.push xs[i]
   return (indexMajorArgs, otherArgs)
 

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) : CommandElabM MessageData := do
+private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) (sig : Bool := true) : CommandElabM MessageData := do
   let m : MessageData :=
     match (← getReducibilityStatus id) with
     | ReducibilityStatus.irreducible => "@[irreducible] "
@@ -38,11 +38,13 @@ 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)
-  let m := m ++ kind ++ " " ++ id ++ levelParamsToMessageData levelParams ++ " : " ++ type
-  pure m
+  if sig then
+    return m!"{m}{kind} {id}{levelParamsToMessageData levelParams} : {type}"
+  else
+    return m!"{m}{kind}"
 
-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 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 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
@@ -65,32 +67,63 @@ 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)
-    (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 := ""
+    (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:"
         for field in fields do
-          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
+          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
 
 private def printIdCore (id : Name) : CommandElabM Unit := do
   let env ← getEnv
@@ -103,11 +136,10 @@ 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, .. } =>
-    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
+    if isStructure env id then
+      printStructure id us numParams t u
+    else
+      printInduct id us numParams t ctors u
   | none => throwUnknownId id
 
 private def printId (id : Syntax) : CommandElabM Unit := do

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].getSepArgs.foldlM (init := none) fun s? arg => do
+  let s? ← stx[2][0].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 <| mkNullNode #[valField]
+    let val       := val.setArg 2 <| mkNode ``Parser.Term.structInstFields #[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 "))
-                 >> sepByIndent (structInstFieldAbbrev <|> structInstField) ...
+                 >> structInstFields (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].getSepArgs.toList.mapM fun fieldStx => do
+  let fields ← stx[2][0].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,7 +602,9 @@ 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 valStx := valStx.setArg 2 (mkNullNode <| mkSepArray args (mkAtom ","))
+            let fieldsStx := mkNode ``Parser.Term.structInstFields
+              #[mkNullNode <| mkSepArray args (mkAtom ",")]
+            let valStx := valStx.setArg 2 fieldsStx
             let valStx ← updateSource valStx
             return { field with lhs := [field.lhs.head!], val := FieldVal.term valStx }
   /--

src/Lean/Elab/Syntax.lean

@@ -236,8 +236,9 @@ where
     -- Pretty-printing instructions shouldn't affect validity
     let s := s.trim
     !s.isEmpty &&
-    (s.front != '\'' || s == "''") &&
+    (s.front != '\'' || "''".isPrefixOf s) &&
     s.front != '\"' &&
+    !(isIdBeginEscape s.front) &&
     !(s.front == '`' && (s.endPos == ⟨1⟩ || isIdFirst (s.get ⟨1⟩) || isIdBeginEscape (s.get ⟨1⟩))) &&
     !s.front.isDigit &&
     !(s.any Char.isWhitespace)

src/Lean/Elab/Tactic/Config.lean

@@ -114,6 +114,13 @@ 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
@@ -148,6 +155,8 @@ 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/LibrarySearch.lean

@@ -40,7 +40,7 @@ def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireCl
     | some suggestions =>
       if requireClose then throwError
         "`exact?` could not close the goal. Try `apply?` to see partial suggestions."
-      reportOutOfHeartbeats `library_search ref
+      reportOutOfHeartbeats `apply? ref
       for (_, suggestionMCtx) in suggestions do
         withMCtx suggestionMCtx do
           addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta (addSubgoalsMsg := true)

src/Lean/Elab/Term.lean

@@ -1298,13 +1298,20 @@ 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,41 +1333,54 @@ def addTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none)
   if (← read).inPattern && !force then
     return mkPatternWithRef e stx
   else
-    withInfoContext' (pure ()) (fun _ => mkTermInfo elaborator stx e expectedType? lctx? isBinder) |> discard
+    discard <| withInfoContext'
+      (pure ())
+      (fun _ => mkTermInfo elaborator stx e expectedType? lctx? isBinder)
+      (mkPartialTermInfo elaborator stx expectedType? lctx?)
     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)) : TermElabM Expr := do
+def withInfoContext' (stx : Syntax) (x : TermElabM Expr)
+    (mkInfo : Expr → TermElabM (Sum Info MVarId)) (mkInfoOnError : TermElabM Info) :
+    TermElabM Expr := do
   if (← read).inPattern then
     let e ← x
     return mkPatternWithRef e stx
   else
-    Elab.withInfoContext' x mkInfo
+    Elab.withInfoContext' x mkInfo mkInfoOnError
 
 /-- Info node capturing `def/let rec` bodies, used by the unused variables linter. -/
 structure BodyInfo where
-  /-- The body as a fully elaborated term. -/
-  value : Expr
+  /-- The body as a fully elaborated term. `none` if the body failed to elaborate. -/
+  value? : Option Expr
 deriving TypeName
 
 /-- Creates an `Info.ofCustomInfo` node backed by a `BodyInfo`. -/
-def mkBodyInfo (stx : Syntax) (value : Expr) : Info :=
-  .ofCustomInfo { stx, value := .mk { value : BodyInfo } }
+def mkBodyInfo (stx : Syntax) (value? : Option 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
-  withInfoContext' stx (mkInfo := mkTermInfo .anonymous (expectedType? := expectedType?) stx) do
+  withTermInfoContext' .anonymous stx (expectedType? := expectedType?) do
     postponeElabTermCore stx expectedType?
 
 /--
@@ -1372,7 +1392,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`)
-      withInfoContext' stx (mkInfo := mkTermInfo elabFn.declName (expectedType? := expectedType?) stx)
+      withTermInfoContext' elabFn.declName stx (expectedType? := expectedType?)
         (try
           elabFn.value stx expectedType?
         catch ex => match ex with
@@ -1755,7 +1775,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?
-      withInfoContext' stx (mkInfo := mkTermInfo decl (expectedType? := expectedType?) stx) <|
+      withTermInfoContext' decl stx (expectedType? := expectedType?) <|
         withMacroExpansion stx stxNew <|
           withRef stxNew <|
             elabTermAux expectedType? catchExPostpone implicitLambda stxNew

src/Lean/Level.lean

@@ -599,17 +599,20 @@ 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
-    | 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
+    | _,          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 ()
   termination_by (u, v)
 
 end Level

src/Lean/Linter/UnusedVariables.lean

@@ -393,16 +393,17 @@ where
         | .ofCustomInfo ti =>
           if !linter.unusedVariables.analyzeTactics.get ci.options then
             if let some bodyInfo := ti.value.get? Elab.Term.BodyInfo 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 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
+              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
         | .ofTermInfo ti =>
           if ignored then return true
           match ti.expr with

src/Lean/Meta/ExprDefEq.lean

@@ -1387,15 +1387,21 @@ 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
-  | Expr.const _ ls₁, Expr.const _ ls₂ => isListLevelDefEq ls₁ ls₂
-  | Expr.app _ _,     Expr.app _ _     =>
+  | .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 _ _     =>
     if (← tryHeuristic t s) then
-      pure LBool.true
+      return .true
     else
       unfold t
-       (unfold s (pure LBool.undef) (fun s => isDefEqRight fn t s))
+       (unfold s (pure .undef) fun s => isDefEqRight fn t s)
        (fun t => unfold s (isDefEqLeft fn t s) (fun s => isDefEqLeftRight fn t s))
-  | _, _ => pure LBool.false
+  | _, _ => return .false
 
 private def sameHeadSymbol (t s : Expr) : Bool :=
   match t.getAppFn, s.getAppFn with
@@ -1674,11 +1680,12 @@ 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₁.isLetVar <||> fvarId₂.isLetVar) then
-      return LBool.undef
-    else if fvarId₁ == fvarId₂ then
-      return LBool.true
+    if fvarId₁ == fvarId₂ then
+      return .true
+    else if (← fvarId₁.isLetVar <||> fvarId₂.isLetVar) then
+      return .undef
     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/Tactic/TryThis.lean

@@ -430,11 +430,13 @@ 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 := do
+private def addExactSuggestionCore (addSubgoalsMsg : Bool) (e : Expr) : MetaM Suggestion :=
+  withOptions (pp.mvars.set · false) do
   let stx ← delabToRefinableSyntax e
   let mvars ← getMVars e
   let suggestion ← if mvars.isEmpty then `(tactic| exact $stx) else `(tactic| refine $stx)
-  let messageData? := if mvars.isEmpty then m!"exact {e}" else m!"refine {e}"
+  let pp ← ppExpr e
+  let messageData? := if mvars.isEmpty then m!"exact {pp}" else m!"refine {pp}"
   let postInfo? ← if !addSubgoalsMsg || mvars.isEmpty then pure none else
     let mut str := "\nRemaining subgoals:"
     for g in mvars do

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" >> sepByIndent (ppGroup whereStructField) "; " (allowTrailingSep := true) >>
+  ppIndent ppSpace >> "where" >> Term.structInstFields (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,6 +281,12 @@ 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:
@@ -292,7 +298,7 @@ The structure type can be specified if not inferable:
 -/
 @[builtin_term_parser] def structInst := leading_parser
   "{ " >> withoutPosition (optional (atomic (sepBy1 termParser ", " >> " with "))
-    >> sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true)
+    >> structInstFields (sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true))
     >> optEllipsis
     >> optional (" : " >> termParser)) >> " }"
 def typeSpec := leading_parser " : " >> termParser
@@ -984,6 +990,7 @@ 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,21 +91,32 @@ Rather, it is called through the `app` delaborator.
 -/
 def delabConst : Delab := do
   let Expr.const c₀ ls ← getExpr | unreachable!
-  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
+  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)
       else
-        c := c₀
-    pure <| mkIdent c
+        -- The name is not defined in this module, so make inaccessible. Unresolving does not make sense to do.
+        c ← withFreshMacroScope <| MonadQuotation.addMacroScope n
   else
-    let mvars ← getPPOption getPPMVarsLevels
-    `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*})
+    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 stx ← maybeAddBlockImplicit stx
   if (← getPPOption getPPTagAppFns) then

src/Lean/Server/Completion/CompletionCollectors.lean

@@ -0,0 +1,610 @@
+/-
+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

@@ -0,0 +1,131 @@
+/-
+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

@@ -0,0 +1,91 @@
+/-
+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

@@ -0,0 +1,22 @@
+/-
+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

@@ -0,0 +1,53 @@
+/-
+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/ImportCompletion.lean

@@ -4,13 +4,10 @@ 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.CompletionItemData
+import Lean.Server.Completion.CompletionItemData
 
 namespace ImportCompletion
 

src/Lean/Server/Completion/SyntheticCompletion.lean

@@ -0,0 +1,396 @@
+/-
+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.ImportCompletion
+import Lean.Server.Completion.ImportCompletion
 
 /-!
 For general server architecture, see `README.md`. For details of IPC communication, see `Watchdog.lean`.

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -46,10 +46,11 @@ 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 := "-"}], isIncomplete := true }
-    if let some r ← Completion.find? p doc.meta.text pos cmdStx infoTree caps then
-      return r
-    return { items := #[ ], isIncomplete := true }
+      | return {
+        items := #[{label := "-", data? := toJson { params := p : Lean.Lsp.CompletionItemData }}],
+        isIncomplete := true
+      }
+    Completion.find? p doc.meta.text pos cmdStx infoTree caps
 
 /--
 Handles `completionItem/resolve` requests that are sent by the client after the user selects
@@ -62,7 +63,7 @@ def handleCompletionItemResolve (item : CompletionItem)
     : RequestM (RequestTask CompletionItem) := do
   let doc ← readDoc
   let text := doc.meta.text
-  let some (data : CompletionItemDataWithId) := item.data?.bind fun data => (fromJson? data).toOption
+  let some (data : ResolvableCompletionItemData) := item.data?.bind fun data => (fromJson? data).toOption
     | return .pure item
   let some id := data.id?
     | return .pure item
@@ -70,7 +71,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
+    Completion.resolveCompletionItem? text pos cmdStx infoTree item id data.cPos
 
 open Elab in
 def handleHover (p : HoverParams)

src/Lean/Server/InfoUtils.lean

@@ -136,6 +136,7 @@ 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
@@ -146,6 +147,7 @@ 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/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -815,7 +815,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
             have k'_in_bounds : k' < acc.2.1.length := by
               simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds
               exact Nat.lt_of_succ_lt_succ k'_succ_in_bounds
-            exact h2 (acc.2.1.get ⟨k', k'_in_bounds⟩) <| List.get_mem acc.snd.fst k' k'_in_bounds
+            exact h2 (acc.2.1.get ⟨k', k'_in_bounds⟩) <| List.get_mem acc.snd.fst ⟨k', k'_in_bounds⟩
     · next l_ne_i =>
       apply Or.inl
       constructor

src/include/lean/lean.h

@@ -406,6 +406,13 @@ static inline unsigned lean_ptr_other(lean_object * o) {
    small objects is a multiple of LEAN_OBJECT_SIZE_DELTA */
 LEAN_EXPORT size_t lean_object_byte_size(lean_object * o);
 
+/* Returns the size of the salient part of an object's storage,
+   i.e. the parts that contribute to the value representation;
+   padding or unused capacity is excluded. Operations that read
+   from an object's storage must only access these parts, since
+   the non-salient parts may not be initialized. */
+LEAN_EXPORT size_t lean_object_data_byte_size(lean_object * o);
+
 static inline bool lean_is_mt(lean_object * o) {
     return o->m_rc < 0;
 }
@@ -695,6 +702,9 @@ static inline size_t lean_array_capacity(b_lean_obj_arg o) { return lean_to_arra
 static inline size_t lean_array_byte_size(lean_object * o) {
     return sizeof(lean_array_object) + sizeof(void*)*lean_array_capacity(o);
 }
+static inline size_t lean_array_data_byte_size(lean_object * o) {
+    return sizeof(lean_array_object) + sizeof(void*)*lean_array_size(o);
+}
 static inline lean_object ** lean_array_cptr(lean_object * o) { return lean_to_array(o)->m_data; }
 static inline void lean_array_set_size(u_lean_obj_arg o, size_t sz) {
     assert(lean_is_array(o));
@@ -852,6 +862,9 @@ static inline size_t lean_sarray_byte_size(lean_object * o) {
     return sizeof(lean_sarray_object) + lean_sarray_elem_size(o)*lean_sarray_capacity(o);
 }
 static inline size_t lean_sarray_size(b_lean_obj_arg o) { return lean_to_sarray(o)->m_size; }
+static inline size_t lean_sarray_data_byte_size(lean_object * o) {
+    return sizeof(lean_sarray_object) + lean_sarray_elem_size(o)*lean_sarray_size(o);
+}
 static inline void lean_sarray_set_size(u_lean_obj_arg o, size_t sz) {
     assert(lean_is_exclusive(o));
     assert(sz <= lean_sarray_capacity(o));
@@ -1013,6 +1026,7 @@ static inline char const * lean_string_cstr(b_lean_obj_arg o) {
 }
 static inline size_t lean_string_size(b_lean_obj_arg o) { return lean_to_string(o)->m_size; }
 static inline size_t lean_string_len(b_lean_obj_arg o) { return lean_to_string(o)->m_length; }
+static inline size_t lean_string_data_byte_size(lean_object * o) { return sizeof(lean_string_object) + lean_string_size(o); }
 LEAN_EXPORT lean_obj_res lean_string_push(lean_obj_arg s, uint32_t c);
 LEAN_EXPORT lean_obj_res lean_string_append(lean_obj_arg s1, b_lean_obj_arg s2);
 static inline lean_obj_res lean_string_length(b_lean_obj_arg s) { return lean_box(lean_string_len(s)); }

src/runtime/object.cpp

@@ -172,6 +172,28 @@ extern "C" LEAN_EXPORT size_t lean_object_byte_size(lean_object * o) {
     }
 }
 
+extern "C" LEAN_EXPORT size_t lean_object_data_byte_size(lean_object * o) {
+    if (o->m_cs_sz == 0) {
+        /* Recall that multi-threaded, single-threaded and persistent objects are stored in the heap.
+           Persistent objects are multi-threaded and/or single-threaded that have been "promoted" to
+           a persistent status. */
+        switch (lean_ptr_tag(o)) {
+        case LeanArray:       return lean_array_data_byte_size(o);
+        case LeanScalarArray: return lean_sarray_data_byte_size(o);
+        case LeanString:      return lean_string_data_byte_size(o);
+        default:              return lean_small_object_size(o);
+        }
+    } else {
+        /* See comment at `lean_set_non_heap_header`, for small objects we store the object size in the RC field. */
+        switch (lean_ptr_tag(o)) {
+        case LeanArray:       return lean_array_data_byte_size(o);
+        case LeanScalarArray: return lean_sarray_data_byte_size(o);
+        case LeanString:      return lean_string_data_byte_size(o);
+        default:              return o->m_cs_sz;
+        }
+    }
+}
+
 static inline void lean_dealloc(lean_object * o, size_t sz) {
 #ifdef LEAN_SMALL_ALLOCATOR
     dealloc(o, sz);

src/runtime/sharecommon.cpp

@@ -13,8 +13,8 @@ namespace lean {
 extern "C" LEAN_EXPORT uint8 lean_sharecommon_eq(b_obj_arg o1, b_obj_arg o2) {
     lean_assert(!lean_is_scalar(o1));
     lean_assert(!lean_is_scalar(o2));
-    size_t sz1 = lean_object_byte_size(o1);
-    size_t sz2 = lean_object_byte_size(o2);
+    size_t sz1 = lean_object_data_byte_size(o1);
+    size_t sz2 = lean_object_data_byte_size(o2);
     if (sz1 != sz2) return false;
     // compare relevant parts of the header
     if (lean_ptr_tag(o1) != lean_ptr_tag(o2)) return false;
@@ -27,7 +27,7 @@ extern "C" LEAN_EXPORT uint8 lean_sharecommon_eq(b_obj_arg o1, b_obj_arg o2) {
 
 extern "C" LEAN_EXPORT uint64_t lean_sharecommon_hash(b_obj_arg o) {
     lean_assert(!lean_is_scalar(o));
-    size_t sz = lean_object_byte_size(o);
+    size_t sz = lean_object_data_byte_size(o);
     size_t header_sz = sizeof(lean_object);
     // hash relevant parts of the header
     unsigned init = hash(lean_ptr_tag(o), lean_ptr_other(o));