chore: fix apply? error reporting when out of heartbeats

This PR fixes a bug where structural recursion did not work when indices
of the recursive argument appeared as function parameters in a different
order than in the argument's type's definition.

Fixes #6015.

src/Init/Data/Array/Find.lean

@@ -0,0 +1,275 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.List.Find
+import Init.Data.Array.Lemmas
+import Init.Data.Array.Attach
+
+/-!
+# Lemmas about `Array.findSome?`, `Array.find?`.
+-/
+
+namespace Array
+
+open Nat
+
+/-! ### findSome? -/
+
+@[simp] theorem findSomeRev?_push_of_isSome (l : Array α) (h : (f a).isSome) : (l.push a).findSomeRev? f = f a := by
+  cases l; simp_all
+
+@[simp] theorem findSomeRev?_push_of_isNone (l : Array α) (h : (f a).isNone) : (l.push a).findSomeRev? f = l.findSomeRev? f := by
+  cases l; simp_all
+
+theorem exists_of_findSome?_eq_some {f : α → Option β} {l : Array α} (w : l.findSome? f = some b) :
+    ∃ a, a ∈ l ∧ f a = b := by
+  cases l; simp_all [List.exists_of_findSome?_eq_some]
+
+@[simp] theorem findSome?_eq_none_iff : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by
+  cases l; simp
+
+@[simp] theorem findSome?_isSome_iff {f : α → Option β} {l : Array α} :
+    (l.findSome? f).isSome ↔ ∃ x, x ∈ l ∧ (f x).isSome := by
+  cases l; simp
+
+theorem findSome?_eq_some_iff {f : α → Option β} {l : Array α} {b : β} :
+    l.findSome? f = some b ↔ ∃ (l₁ : Array α) (a : α) (l₂ : Array α), l = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ x ∈ l₁, f x = none := by
+  cases l
+  simp only [List.findSome?_toArray, List.findSome?_eq_some_iff]
+  constructor
+  · rintro ⟨l₁, a, l₂, rfl, h₁, h₂⟩
+    exact ⟨l₁.toArray, a, l₂.toArray, by simp_all⟩
+  · rintro ⟨l₁, a, l₂, h₀, h₁, h₂⟩
+    exact ⟨l₁.toList, a, l₂.toList, by simpa using congrArg toList h₀, h₁, by simpa⟩
+
+@[simp] theorem findSome?_guard (l : Array α) : findSome? (Option.guard fun x => p x) l = find? p l := by
+  cases l; simp
+
+@[simp] theorem getElem?_zero_filterMap (f : α → Option β) (l : Array α) : (l.filterMap f)[0]? = l.findSome? f := by
+  cases l; simp [← List.head?_eq_getElem?]
+
+@[simp] theorem getElem_zero_filterMap (f : α → Option β) (l : Array α) (h) :
+    (l.filterMap f)[0] = (l.findSome? f).get (by cases l; simpa [List.length_filterMap_eq_countP] using h) := by
+  cases l; simp [← List.head_eq_getElem, ← getElem?_zero_filterMap]
+
+@[simp] theorem back?_filterMap (f : α → Option β) (l : Array α) : (l.filterMap f).back? = l.findSomeRev? f := by
+  cases l; simp
+
+@[simp] theorem back!_filterMap [Inhabited β] (f : α → Option β) (l : Array α) :
+    (l.filterMap f).back! = (l.findSomeRev? f).getD default := by
+  cases l; simp
+
+@[simp] theorem map_findSome? (f : α → Option β) (g : β → γ) (l : Array α) :
+    (l.findSome? f).map g = l.findSome? (Option.map g ∘ f) := by
+  cases l; simp
+
+theorem findSome?_map (f : β → γ) (l : Array β) : findSome? p (l.map f) = l.findSome? (p ∘ f) := by
+  cases l; simp [List.findSome?_map]
+
+theorem findSome?_append {l₁ l₂ : Array α} : (l₁ ++ l₂).findSome? f = (l₁.findSome? f).or (l₂.findSome? f) := by
+  cases l₁; cases l₂; simp [List.findSome?_append]
+
+theorem getElem?_zero_flatten (L : Array (Array α)) :
+    (flatten L)[0]? = L.findSome? fun l => l[0]? := by
+  cases L using array_array_induction
+  simp [← List.head?_eq_getElem?, List.head?_flatten, List.findSome?_map, Function.comp_def]
+
+theorem getElem_zero_flatten.proof {L : Array (Array α)} (h : 0 < L.flatten.size) :
+    (L.findSome? fun l => l[0]?).isSome := by
+  cases L using array_array_induction
+  simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray,
+    List.findSome?_isSome_iff, List.isSome_getElem?]
+  simp only [flatten_toArray_map_toArray, size_toArray, List.length_flatten,
+    Nat.sum_pos_iff_exists_pos, List.mem_map] at h
+  obtain ⟨_, ⟨xs, m, rfl⟩, h⟩ := h
+  exact ⟨xs, m, by simpa using h⟩
+
+theorem getElem_zero_flatten {L : Array (Array α)} (h) :
+    (flatten L)[0] = (L.findSome? fun l => l[0]?).get (getElem_zero_flatten.proof h) := by
+  have t := getElem?_zero_flatten L
+  simp [getElem?_eq_getElem, h] at t
+  simp [← t]
+
+theorem back?_flatten {L : Array (Array α)} :
+    (flatten L).back? = (L.findSomeRev? fun l => l.back?) := by
+  cases L using array_array_induction
+  simp [List.getLast?_flatten, ← List.map_reverse, List.findSome?_map, Function.comp_def]
+
+theorem findSome?_mkArray : findSome? f (mkArray n a) = if n = 0 then none else f a := by
+  simp [mkArray_eq_toArray_replicate, List.findSome?_replicate]
+
+@[simp] theorem findSome?_mkArray_of_pos (h : 0 < n) : findSome? f (mkArray n a) = f a := by
+  simp [findSome?_mkArray, Nat.ne_of_gt h]
+
+-- Argument is unused, but used to decide whether `simp` should unfold.
+@[simp] theorem findSome?_mkArray_of_isSome (_ : (f a).isSome) :
+   findSome? f (mkArray n a) = if n = 0 then none else f a := by
+  simp [findSome?_mkArray]
+
+@[simp] theorem findSome?_mkArray_of_isNone (h : (f a).isNone) :
+    findSome? f (mkArray n a) = none := by
+  rw [Option.isNone_iff_eq_none] at h
+  simp [findSome?_mkArray, h]
+
+/-! ### find? -/
+
+@[simp] theorem find?_singleton (a : α) (p : α → Bool) :
+    #[a].find? p = if p a then some a else none := by
+  simp [singleton_eq_toArray_singleton]
+
+@[simp] theorem findRev?_push_of_pos (l : Array α) (h : p a) :
+    findRev? p (l.push a) = some a := by
+  cases l; simp [h]
+
+@[simp] theorem findRev?_cons_of_neg (l : Array α) (h : ¬p a) :
+    findRev? p (l.push a) = findRev? p l := by
+  cases l; simp [h]
+
+@[simp] theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x := by
+  cases l; simp
+
+theorem find?_eq_some_iff_append {xs : Array α} :
+    xs.find? p = some b ↔ p b ∧ ∃ (as bs : Array α), xs = as.push b ++ bs ∧ ∀ a ∈ as, !p a := by
+  rcases xs with ⟨xs⟩
+  simp only [List.find?_toArray, List.find?_eq_some_iff_append, Bool.not_eq_eq_eq_not,
+    Bool.not_true, exists_and_right, and_congr_right_iff]
+  intro w
+  constructor
+  · rintro ⟨as, ⟨⟨x, rfl⟩, h⟩⟩
+    exact ⟨as.toArray, ⟨x.toArray, by simp⟩ , by simpa using h⟩
+  · rintro ⟨as, ⟨⟨x, h'⟩, h⟩⟩
+    exact ⟨as.toList, ⟨x.toList, by simpa using congrArg Array.toList h'⟩,
+      by simpa using h⟩
+
+@[simp]
+theorem find?_push_eq_some {xs : Array α} :
+    (xs.push a).find? p = some b ↔ xs.find? p = some b ∨ (xs.find? p = none ∧ (p a ∧ a = b)) := by
+  cases xs; simp
+
+@[simp] theorem find?_isSome {xs : Array α} {p : α → Bool} : (xs.find? p).isSome ↔ ∃ x, x ∈ xs ∧ p x := by
+  cases xs; simp
+
+theorem find?_some {xs : Array α} (h : find? p xs = some a) : p a := by
+  cases xs
+  simp at h
+  exact List.find?_some h
+
+theorem mem_of_find?_eq_some {xs : Array α} (h : find? p xs = some a) : a ∈ xs := by
+  cases xs
+  simp at h
+  simpa using List.mem_of_find?_eq_some h
+
+theorem get_find?_mem {xs : Array α} (h) : (xs.find? p).get h ∈ xs := by
+  cases xs
+  simp [List.get_find?_mem]
+
+@[simp] theorem find?_filter {xs : Array α} (p q : α → Bool) :
+    (xs.filter p).find? q = xs.find? (fun a => p a ∧ q a) := by
+  cases xs; simp
+
+@[simp] theorem getElem?_zero_filter (p : α → Bool) (l : Array α) :
+    (l.filter p)[0]? = l.find? p := by
+  cases l; simp [← List.head?_eq_getElem?]
+
+@[simp] theorem getElem_zero_filter (p : α → Bool) (l : Array α) (h) :
+    (l.filter p)[0] =
+      (l.find? p).get (by cases l; simpa [← List.countP_eq_length_filter] using h) := by
+  cases l
+  simp [List.getElem_zero_eq_head]
+
+@[simp] theorem back?_filter (p : α → Bool) (l : Array α) : (l.filter p).back? = l.findRev? p := by
+  cases l; simp
+
+@[simp] theorem back!_filter [Inhabited α] (p : α → Bool) (l : Array α) :
+    (l.filter p).back! = (l.findRev? p).get! := by
+  cases l; simp [Option.get!_eq_getD]
+
+@[simp] theorem find?_filterMap (xs : Array α) (f : α → Option β) (p : β → Bool) :
+    (xs.filterMap f).find? p = (xs.find? (fun a => (f a).any p)).bind f := by
+  cases xs; simp
+
+@[simp] theorem find?_map (f : β → α) (xs : Array β) :
+    find? p (xs.map f) = (xs.find? (p ∘ f)).map f := by
+  cases xs; simp
+
+@[simp] theorem find?_append {l₁ l₂ : Array α} :
+    (l₁ ++ l₂).find? p = (l₁.find? p).or (l₂.find? p) := by
+  cases l₁
+  cases l₂
+  simp
+
+@[simp] theorem find?_flatten (xs : Array (Array α)) (p : α → Bool) :
+    xs.flatten.find? p = xs.findSome? (·.find? p) := by
+  cases xs using array_array_induction
+  simp [List.findSome?_map, Function.comp_def]
+
+theorem find?_flatten_eq_none {xs : Array (Array α)} {p : α → Bool} :
+    xs.flatten.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x := by
+  simp
+
+/--
+If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
+some array in `xs` contains `a`, and no earlier element of that array satisfies `p`.
+Moreover, no earlier array in `xs` has an element satisfying `p`.
+-/
+theorem find?_flatten_eq_some {xs : Array (Array α)} {p : α → Bool} {a : α} :
+    xs.flatten.find? p = some a ↔
+      p a ∧ ∃ (as : Array (Array α)) (ys zs : Array α) (bs : Array (Array α)),
+        xs = as.push (ys.push a ++ zs) ++ bs ∧
+        (∀ a ∈ as, ∀ x ∈ a, !p x) ∧ (∀ x ∈ ys, !p x) := by
+  cases xs using array_array_induction
+  simp only [flatten_toArray_map_toArray, List.find?_toArray, List.find?_flatten_eq_some]
+  simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, and_congr_right_iff]
+  intro w
+  constructor
+  · rintro ⟨as, ys, ⟨⟨zs, bs, rfl⟩, h₁, h₂⟩⟩
+    exact ⟨as.toArray.map List.toArray, ys.toArray,
+      ⟨zs.toArray, bs.toArray.map List.toArray, by simp⟩, by simpa using h₁, by simpa using h₂⟩
+  · rintro ⟨as, ys, ⟨⟨zs, bs, h⟩, h₁, h₂⟩⟩
+    replace h := congrArg (·.map Array.toList) (congrArg Array.toList h)
+    simp [Function.comp_def] at h
+    exact ⟨as.toList.map Array.toList, ys.toList,
+      ⟨zs.toList, bs.toList.map Array.toList, by simpa using h⟩,
+        by simpa using h₁, by simpa using h₂⟩
+
+@[simp] theorem find?_flatMap (xs : Array α) (f : α → Array β) (p : β → Bool) :
+    (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
+  cases xs
+  simp [List.find?_flatMap, Array.flatMap_toArray]
+
+theorem find?_flatMap_eq_none {xs : Array α} {f : α → Array β} {p : β → Bool} :
+    (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
+  simp
+
+theorem find?_mkArray :
+    find? p (mkArray n a) = if n = 0 then none else if p a then some a else none := by
+  simp [mkArray_eq_toArray_replicate, List.find?_replicate]
+
+@[simp] theorem find?_mkArray_of_length_pos (h : 0 < n) :
+    find? p (mkArray n a) = if p a then some a else none := by
+  simp [find?_mkArray, Nat.ne_of_gt h]
+
+@[simp] theorem find?_mkArray_of_pos (h : p a) :
+    find? p (mkArray n a) = if n = 0 then none else some a := by
+  simp [find?_mkArray, h]
+
+@[simp] theorem find?_mkArray_of_neg (h : ¬ p a) : find? p (mkArray n a) = none := by
+  simp [find?_mkArray, h]
+
+-- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
+theorem find?_mkArray_eq_none {n : Nat} {a : α} {p : α → Bool} :
+    (mkArray n a).find? p = none ↔ n = 0 ∨ !p a := by
+  simp [mkArray_eq_toArray_replicate, List.find?_replicate_eq_none, Classical.or_iff_not_imp_left]
+
+@[simp] theorem find?_mkArray_eq_some {n : Nat} {a b : α} {p : α → Bool} :
+    (mkArray n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
+  simp [mkArray_eq_toArray_replicate]
+
+@[simp] theorem get_find?_mkArray (n : Nat) (a : α) (p : α → Bool) (h) :
+    ((mkArray n a).find? p).get h = a := by
+  simp [mkArray_eq_toArray_replicate]
+
+end Array

src/Init/Data/Array/Lemmas.lean

@@ -601,7 +601,7 @@ theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
 
 /-- # mem -/
 
-theorem mem_toList {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l := mem_def.symm
+@[simp] theorem mem_toList {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l := mem_def.symm
 
 theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
 
@@ -620,19 +620,19 @@ theorem getElem?_of_mem {a : α} {as : Array α} :
 
 @[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 [mem_def]
+  split <;> simp_all
 
 @[simp] theorem mem_dite_empty_right {x : α} [Decidable p] {l : p → Array α} :
     (x ∈ if h : p then l h else #[]) ↔ ∃ h : p, x ∈ l h := by
-  split <;> simp_all [mem_def]
+  split <;> simp_all
 
 @[simp] theorem mem_ite_empty_left {x : α} [Decidable p] {l : Array α} :
     (x ∈ if p then #[] else l) ↔ ¬ p ∧ x ∈ l := by
-  split <;> simp_all [mem_def]
+  split <;> simp_all
 
 @[simp] theorem mem_ite_empty_right {x : α} [Decidable p] {l : Array α} :
     (x ∈ if p then l else #[]) ↔ p ∧ x ∈ l := by
-  split <;> simp_all [mem_def]
+  split <;> simp_all
 
 /-- # get lemmas -/
 
@@ -1218,6 +1218,14 @@ theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] :=
 @[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
   simp only [size, toList_append, List.length_append]
 
+@[simp] theorem empty_append (as : Array α) : #[] ++ as = as := by
+  cases as
+  simp
+
+@[simp] theorem append_empty (as : Array α) : as ++ #[] = as := by
+  cases as
+  simp
+
 theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
     (as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by
   cases as; cases bs
@@ -1876,6 +1884,50 @@ namespace Array
   induction as
   simp
 
+/-! ### map -/
+
+@[simp] theorem map_map {f : α → β} {g : β → γ} {as : Array α} :
+    (as.map f).map g = as.map (g ∘ f) := by
+  cases as; simp
+
+@[simp] theorem map_id_fun : map (id : α → α) = id := by
+  funext l
+  induction l <;> simp_all
+
+/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/
+@[simp] theorem map_id_fun' : map (fun (a : α) => a) = id := map_id_fun
+
+-- This is not a `@[simp]` lemma because `map_id_fun` will apply.
+theorem map_id (as : Array α) : map (id : α → α) as = as := by
+  cases as <;> simp_all
+
+/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/
+-- This is not a `@[simp]` lemma because `map_id_fun'` will apply.
+theorem map_id' (as : Array α) : map (fun (a : α) => a) as = as := map_id as
+
+/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/
+theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (as : Array α) : map f as = as := by
+  simp [show f = id from funext h]
+
+theorem array_array_induction (P : Array (Array α) → Prop) (h : ∀ (xss : List (List α)), P (xss.map List.toArray).toArray)
+    (ass : Array (Array α)) : P ass := by
+  specialize h (ass.toList.map toList)
+  simpa [← toList_map, Function.comp_def, map_id] using h
+
+/-! ### flatten -/
+
+@[simp] theorem flatten_empty : flatten (#[] : Array (Array α)) = #[] := rfl
+
+@[simp] theorem flatten_toArray_map_toArray (xss : List (List α)) :
+    (xss.map List.toArray).toArray.flatten = xss.flatten.toArray := by
+  simp [flatten]
+  suffices ∀ as, List.foldl (fun r a => r ++ a) as (List.map List.toArray xss) = as ++ xss.flatten.toArray by
+    simpa using this #[]
+  intro as
+  induction xss generalizing as with
+  | nil => simp
+  | cons xs xss ih => simp [ih]
+
 /-! ### findSomeRevM?, findRevM?, findSomeRev?, findRev? -/
 
 @[simp] theorem findSomeRevM?_eq_findSomeM?_reverse
@@ -1940,6 +1992,27 @@ namespace Array
   cases as
   simp
 
+@[simp] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl
+
+@[simp] theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) :
+    (a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f := by
+  simp [flatMap]
+  suffices ∀ cs, List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as =
+      f a ++ List.foldl (fun bs a => bs ++ f a) cs as by
+    erw [empty_append] -- Why doesn't this work via `simp`?
+    simpa using this #[]
+  intro cs
+  induction as generalizing cs <;> simp_all
+
+@[simp] theorem flatMap_toArray {β} (f : α → Array β) (as : List α) :
+    as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray := by
+  induction as with
+  | nil => simp
+  | cons a as ih =>
+    apply ext'
+    simp [ih]
+
+
 end Array
 
 /-! ### Deprecations -/

src/Init/Data/BitVec/Bitblast.lean

@@ -403,7 +403,7 @@ theorem getLsbD_neg {i : Nat} {x : BitVec w} :
       rw [carry_succ_one _ _ (by omega), ← Bool.xor_not, ← decide_not]
       simp only [add_one_ne_zero, decide_false, getLsbD_not, and_eq_true, decide_eq_true_eq,
         not_eq_eq_eq_not, Bool.not_true, false_bne, not_exists, _root_.not_and, not_eq_true,
-        bne_left_inj, decide_eq_decide]
+        bne_right_inj, decide_eq_decide]
       constructor
       · rintro h j hj; exact And.right <| h j (by omega)
       · rintro h j hj; exact ⟨by omega, h j (by omega)⟩
@@ -419,7 +419,7 @@ theorem getMsbD_neg {i : Nat} {x : BitVec w} :
     simp [hi]; omega
   case pos =>
     have h₁ : w - 1 - i < w := by omega
-    simp only [hi, decide_true, h₁, Bool.true_and, Bool.bne_left_inj, decide_eq_decide]
+    simp only [hi, decide_true, h₁, Bool.true_and, Bool.bne_right_inj, decide_eq_decide]
     constructor
     · rintro ⟨j, hj, h⟩
       refine ⟨w - 1 - j, by omega, by omega, by omega, _root_.cast ?_ h⟩

src/Init/Data/Bool.lean

@@ -238,8 +238,8 @@ theorem not_bne_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by simp
 @[simp] theorem bne_assoc : ∀ (x y z : Bool), ((x != y) != z) = (x != (y != z)) := by decide
 instance : Std.Associative (· != ·) := ⟨bne_assoc⟩
 
-@[simp] theorem bne_left_inj  : ∀ {x y z : Bool}, (x != y) = (x != z) ↔ y = z := by decide
-@[simp] theorem bne_right_inj : ∀ {x y z : Bool}, (x != z) = (y != z) ↔ x = y := by decide
+@[simp] theorem bne_right_inj  : ∀ {x y z : Bool}, (x != y) = (x != z) ↔ y = z := by decide
+@[simp] theorem bne_left_inj : ∀ {x y z : Bool}, (x != z) = (y != z) ↔ x = y := by decide
 
 theorem eq_not_of_ne : ∀ {x y : Bool}, x ≠ y → x = !y := by decide
 
@@ -295,9 +295,9 @@ theorem xor_right_comm : ∀ (x y z : Bool), ((x ^^ y) ^^ z) = ((x ^^ z) ^^ y) :
 
 theorem xor_assoc : ∀ (x y z : Bool), ((x ^^ y) ^^ z) = (x ^^ (y ^^ z)) := bne_assoc
 
-theorem xor_left_inj : ∀ {x y z : Bool}, (x ^^ y) = (x ^^ z) ↔ y = z := bne_left_inj
+theorem xor_right_inj : ∀ {x y z : Bool}, (x ^^ y) = (x ^^ z) ↔ y = z := bne_right_inj
 
-theorem xor_right_inj : ∀ {x y z : Bool}, (x ^^ z) = (y ^^ z) ↔ x = y := bne_right_inj
+theorem xor_left_inj : ∀ {x y z : Bool}, (x ^^ z) = (y ^^ z) ↔ x = y := bne_left_inj
 
 /-! ### le/lt -/
 

src/Init/Data/Float.lean

@@ -53,7 +53,7 @@ Raw transmutation from `UInt64`.
 Floats and UInts have the same endianness on all supported platforms.
 IEEE 754 very precisely specifies the bit layout of floats.
 -/
-@[extern "lean_float_from_bits"] opaque Float.fromBits : UInt64 → Float
+@[extern "lean_float_of_bits"] opaque Float.ofBits : UInt64 → Float
 
 /--
 Raw transmutation to `UInt64`.

src/Init/Data/Int/Lemmas.lean

@@ -329,22 +329,22 @@ theorem toNat_sub (m n : Nat) : toNat (m - n) = m - n := by
 /- ## add/sub injectivity -/
 
 @[simp]
-protected theorem add_right_inj {i j : Int} (k : Int) : (i + k = j + k) ↔ i = j := by
+protected theorem add_left_inj {i j : Int} (k : Int) : (i + k = j + k) ↔ i = j := by
   apply Iff.intro
   · intro p
     rw [←Int.add_sub_cancel i k, ←Int.add_sub_cancel j k, p]
   · exact congrArg (· + k)
 
 @[simp]
-protected theorem add_left_inj {i j : Int} (k : Int) : (k + i = k + j) ↔ i = j := by
+protected theorem add_right_inj {i j : Int} (k : Int) : (k + i = k + j) ↔ i = j := by
   simp [Int.add_comm k]
 
 @[simp]
-protected theorem sub_left_inj {i j : Int} (k : Int) : (k - i = k - j) ↔ i = j := by
+protected theorem sub_right_inj {i j : Int} (k : Int) : (k - i = k - j) ↔ i = j := by
   simp [Int.sub_eq_add_neg, Int.neg_inj]
 
 @[simp]
-protected theorem sub_right_inj {i j : Int} (k : Int) : (i - k = j - k) ↔ i = j := by
+protected theorem sub_left_inj {i j : Int} (k : Int) : (i - k = j - k) ↔ i = j := by
   simp [Int.sub_eq_add_neg]
 
 /- ## Ring properties -/

src/Init/Data/List/Lemmas.lean

@@ -372,6 +372,17 @@ theorem getElem?_concat_length (l : List α) (a : α) : (l ++ [a])[l.length]? =
 @[deprecated getElem?_concat_length (since := "2024-06-12")]
 theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = some a := by simp
 
+@[simp] theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length := by
+  by_cases h : n < l.length
+  · simp_all
+  · simp [h]
+    simp_all
+
+@[simp] theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone ↔ l.length ≤ n := by
+  by_cases h : n < l.length
+  · simp_all
+  · simp [h]
+
 /-! ### mem -/
 
 @[simp] theorem not_mem_nil (a : α) : ¬ a ∈ [] := nofun
@@ -1025,6 +1036,10 @@ theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []),
   | _ :: _ :: _, _ => by
     simp [getLast, get, Nat.succ_sub_succ, getLast_eq_getElem]
 
+theorem getElem_length_sub_one_eq_getLast (l : List α) (h) :
+    l[l.length - 1] = getLast l (by cases l; simp at h; simp) := by
+  rw [← getLast_eq_getElem]
+
 @[deprecated getLast_eq_getElem (since := "2024-07-15")]
 theorem getLast_eq_get (l : List α) (h : l ≠ []) :
     getLast l h = l.get ⟨l.length - 1, by
@@ -1149,6 +1164,11 @@ theorem head_eq_getElem (l : List α) (h : l ≠ []) : head l h = l[0]'(length_p
   | nil => simp at h
   | cons _ _ => simp
 
+theorem getElem_zero_eq_head (l : List α) (h) : l[0] = head l (by simpa [length_pos] using h) := by
+  cases l with
+  | nil => simp at h
+  | cons _ _ => simp
+
 theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a ↔ xs.head? = some a := by
   cases xs with
   | nil => simp at h

src/Init/Data/Nat/Lemmas.lean

@@ -1029,3 +1029,12 @@ instance decidableExistsLT [h : DecidablePred p] : DecidablePred fun n => ∃ m
 instance decidableExistsLE [DecidablePred p] : DecidablePred fun n => ∃ m : Nat, m ≤ n ∧ p m :=
   fun n => decidable_of_iff (∃ m, m < n + 1 ∧ p m)
     (exists_congr fun _ => and_congr_left' Nat.lt_succ_iff)
+
+/-! ### Results about `List.sum` specialized to `Nat` -/
+
+protected theorem sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum ↔ ∃ x ∈ l, 0 < x := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp [← ih]
+    omega

src/Init/Data/Option/Lemmas.lean

@@ -55,7 +55,9 @@ theorem get_eq_getD {fallback : α} : (o : Option α) → {h : o.isSome} → o.g
 theorem some_get! [Inhabited α] : (o : Option α) → o.isSome → some (o.get!) = o
   | some _, _ => rfl
 
-theorem get!_eq_getD_default [Inhabited α] (o : Option α) : o.get! = o.getD default := rfl
+theorem get!_eq_getD [Inhabited α] (o : Option α) : o.get! = o.getD default := rfl
+
+@[deprecated get!_eq_getD (since := "2024-11-18")] abbrev get!_eq_getD_default := @get!_eq_getD
 
 theorem mem_unique {o : Option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) : a = b :=
   some.inj <| ha ▸ hb

src/Init/System/IO.lean

@@ -802,6 +802,9 @@ def run (args : SpawnArgs) : IO String := do
 
 end Process
 
+/-- Returns the thread ID of the calling thread. -/
+@[extern "lean_io_get_tid"] opaque getTID : BaseIO UInt64
+
 structure AccessRight where
   read : Bool := false
   write : Bool := false

src/Init/Tactics.lean

@@ -1155,7 +1155,7 @@ Configuration for the `decide` tactic family.
 structure DecideConfig where
   /-- If true (default: false), then use only kernel reduction when reducing the `Decidable` instance.
   This is more efficient, since the default mode reduces twice (once in the elaborator and again in the kernel),
-  however kernel reduction ignores transparency settings. The `decide!` tactic is a synonym for `decide +kernel`. -/
+  however kernel reduction ignores transparency settings. -/
   kernel : Bool := false
   /-- If true (default: false), then uses the native code compiler to evaluate the `Decidable` instance,
   admitting the result via the axiom `Lean.ofReduceBool`.  This can be significantly more efficient,
@@ -1165,7 +1165,9 @@ structure DecideConfig where
   native : Bool := false
   /-- If true (default: true), then when preprocessing the goal, do zeta reduction to attempt to eliminate free variables. -/
   zetaReduce : Bool := true
-  /-- If true (default: false), then when preprocessing reverts free variables. -/
+  /-- If true (default: false), then when preprocessing, removes irrelevant variables and reverts the local context.
+  A variable is *relevant* if it appears in the target, if it appears in a relevant variable,
+  or if it is a proposition that refers to a relevant variable. -/
   revert : Bool := false
 
 /--
@@ -1240,17 +1242,6 @@ example : 1 + 1 = 2 := by rfl
 -/
 syntax (name := decide) "decide" optConfig : tactic
 
-/--
-`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.
-It has the following properties:
-- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.
-- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,
-  and once during kernel type checking), the `decide!` tactic reduces it exactly once.
-
-The `decide!` syntax is short for `decide +kernel`.
--/
-syntax (name := decideBang) "decide!" optConfig : tactic
-
 /--
 `native_decide` is a synonym for `decide +native`.
 It will attempt to prove a goal of type `p` by synthesizing an instance

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/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/StructInst.lean

@@ -11,21 +11,40 @@ import Lean.Elab.App
 import Lean.Elab.Binders
 import Lean.PrettyPrinter
 
+/-!
+# Structure instance elaborator
+
+A *structure instance* is notation to construct a term of a `structure`.
+Examples: `{ x := 2, y.z := true }`, `{ s with cache := c' }`, and `{ s with values[2] := v }`.
+Structure instances are the preferred way to invoke a `structure`'s constructor,
+since they hide Lean implementation details such as whether parents are represented as subobjects,
+and also they do correct processing of default values, which are complicated due to the fact that `structure`s can override default values of their parents.
+
+This module elaborates structure instance notation.
+Note that the `where` syntax to define structures (`Lean.Parser.Command.whereStructInst`)
+macro expands into the structure instance notation elaborated by this module.
+-/
+
 namespace Lean.Elab.Term.StructInst
 
 open Meta
 open TSyntax.Compat
 
-/-
-  Structure instances are of the form:
-
-      "{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
-          >> manyIndent (group ((structInstFieldAbbrev <|> structInstField) >> optional ", "))
-          >> optEllipsis
-          >> optional (" : " >> termParser)
-          >> " }"
+/-!
+Recall that structure instances are of the form:
+```
+"{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
+    >> manyIndent (group ((structInstFieldAbbrev <|> structInstField) >> optional ", "))
+    >> optEllipsis
+    >> optional (" : " >> termParser)
+    >> " }"
+```
 -/
 
+/--
+Transforms structure instances such as `{ x := 0 : Foo }` into `({ x := 0 } : Foo)`.
+Structure instance notation makes use of the expected type.
+-/
 @[builtin_macro Lean.Parser.Term.structInst] def expandStructInstExpectedType : Macro := fun stx =>
   let expectedArg := stx[4]
   if expectedArg.isNone then
@@ -35,7 +54,10 @@ open TSyntax.Compat
     let stxNew   := stx.setArg 4 mkNullNode
     `(($stxNew : $expected))
 
-/-- Expand field abbreviations. Example: `{ x, y := 0 }` expands to `{ x := x, y := 0 }` -/
+/--
+Expands field abbreviation notation.
+Example: `{ x, y := 0 }` expands to `{ x := x, y := 0 }`.
+-/
 @[builtin_macro Lean.Parser.Term.structInst] def expandStructInstFieldAbbrev : Macro
   | `({ $[$srcs,* with]? $fields,* $[..%$ell]? $[: $ty]? }) =>
     if fields.getElems.raw.any (·.getKind == ``Lean.Parser.Term.structInstFieldAbbrev) then do
@@ -49,9 +71,12 @@ open TSyntax.Compat
   | _ => Macro.throwUnsupported
 
 /--
-  If `stx` is of the form `{ s₁, ..., sₙ with ... }` and `sᵢ` is not a local variable, expand into `let src := sᵢ; { ..., src, ... with ... }`.
+If `stx` is of the form `{ s₁, ..., sₙ with ... }` and `sᵢ` is not a local variable,
+expands into `let __src := sᵢ; { ..., __src, ... with ... }`.
+The significance of `__src` is that the variable is treated as an implementation-detail local variable,
+which can be unfolded by `simp` when `zetaDelta := false`.
 
-  Note that this one is not a `Macro` because we need to access the local context.
+Note that this one is not a `Macro` because we need to access the local context.
 -/
 private def expandNonAtomicExplicitSources (stx : Syntax) : TermElabM (Option Syntax) := do
   let sourcesOpt := stx[1]
@@ -100,27 +125,44 @@ where
           let r ← go sources (sourcesNew.push sourceNew)
           `(let __src := $source; $r)
 
-structure ExplicitSourceInfo where
+/--
+An *explicit source* is one of the structures `sᵢ` that appear in `{ s₁, …, sₙ with … }`.
+-/
+structure ExplicitSourceView where
+  /-- The syntax of the explicit source. -/
   stx        : Syntax
+  /-- The name of the structure for the type of the explicit source. -/
   structName : Name
   deriving Inhabited
 
-structure Source where
-  explicit : Array ExplicitSourceInfo -- `s₁ ... sₙ with`
-  implicit : Option Syntax -- `..`
+/--
+A view of the sources of fields for the structure instance notation.
+-/
+structure SourcesView where
+  /-- Explicit sources (i.e., one of the structures `sᵢ` that appear in `{ s₁, …, sₙ with … }`). -/
+  explicit : Array ExplicitSourceView
+  /-- The syntax for a trailing `..`. This is "ellipsis mode" for missing fields, similar to ellipsis mode for applications. -/
+  implicit : Option Syntax
   deriving Inhabited
 
-def Source.isNone : Source → Bool
+/-- Returns `true` if the structure instance has no sources (neither explicit sources nor a `..`). -/
+def SourcesView.isNone : SourcesView → Bool
   | { explicit := #[], implicit := none } => true
   | _ => false
 
-/-- `optional (atomic (sepBy1 termParser ", " >> " with ")` -/
+/--
+Given an array of explicit sources, returns syntax of the form
+`optional (atomic (sepBy1 termParser ", " >> " with ")`
+-/
 private def mkSourcesWithSyntax (sources : Array Syntax) : Syntax :=
   let ref := sources[0]!
   let stx := Syntax.mkSep sources (mkAtomFrom ref ", ")
   mkNullNode #[stx, mkAtomFrom ref "with "]
 
-private def getStructSource (structStx : Syntax) : TermElabM Source :=
+/--
+Creates a structure source view from structure instance notation.
+-/
+private def getStructSources (structStx : Syntax) : TermElabM SourcesView :=
   withRef structStx do
     let explicitSource := structStx[1]
     let implicitSource := structStx[3]
@@ -138,10 +180,10 @@ private def getStructSource (structStx : Syntax) : TermElabM Source :=
     return { explicit, implicit }
 
 /--
-  We say a `{ ... }` notation is a `modifyOp` if it contains only one
-  ```
-  def structInstArrayRef := leading_parser "[" >> termParser >>"]"
-  ```
+We say a structure instance notation is a "modifyOp" if it contains only a single array update.
+```lean
+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
@@ -177,7 +219,11 @@ private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
   | none   => return none
   | some s => if s[0][0].getKind == ``Lean.Parser.Term.structInstArrayRef then return s? else return none
 
-private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSourceInfo) (expectedType? : Option Expr) : TermElabM Expr := do
+/--
+Given a `stx` that is a structure instance notation that's a modifyOp (according to `isModifyOp?`), elaborates it.
+Only supports structure instances with a single source.
+-/
+private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSourceView) (expectedType? : Option Expr) : TermElabM Expr := do
   if sources.size > 1 then
     throwError "invalid \{...} notation, multiple sources and array update is not supported."
   let cont (val : Syntax) : TermElabM Expr := do
@@ -204,12 +250,13 @@ private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSource
     cont val
 
 /--
-  Get structure name.
-  This method triest to postpone execution if the expected type is not available.
+Gets the structure name for the structure instance from the expected type and the sources.
+This method tries to postpone execution if the expected type is not available.
 
-  If the expected type is available and it is a structure, then we use it.
-  Otherwise, we use the type of the first source. -/
-private def getStructName (expectedType? : Option Expr) (sourceView : Source) : TermElabM Name := do
+If the expected type is available and it is a structure, then we use it.
+Otherwise, we use the type of the first source.
+-/
+private def getStructName (expectedType? : Option Expr) (sourceView : SourcesView) : TermElabM Name := do
   tryPostponeIfNoneOrMVar expectedType?
   let useSource : Unit → TermElabM Name := fun _ => do
     unless sourceView.explicit.isEmpty do
@@ -226,7 +273,7 @@ private def getStructName (expectedType? : Option Expr) (sourceView : Source) :
       unless isStructure (← getEnv) constName do
         throwError "invalid \{...} notation, structure type expected{indentExpr expectedType}"
       return constName
-    | _                        => useSource ()
+    | _ => useSource ()
 where
   throwUnknownExpectedType :=
     throwError "invalid \{...} notation, expected type is not known"
@@ -237,72 +284,92 @@ where
     else
       throwError "invalid \{...} notation, {kind} type is not of the form (C ...){indentExpr type}"
 
+/--
+A component of a left-hand side for a field appearing in structure instance syntax.
+-/
 inductive FieldLHS where
+  /-- A name component for a field left-hand side. For example, `x` and `y` in `{ x.y := v }`. -/
   | fieldName  (ref : Syntax) (name : Name)
+  /-- A numeric index component for a field left-hand side. For example `3` in `{ x.3 := v }`. -/
   | fieldIndex (ref : Syntax) (idx : Nat)
+  /-- An array indexing component for a field left-hand side. For example `[3]` in `{ arr[3] := v }`. -/
   | modifyOp   (ref : Syntax) (index : Syntax)
   deriving Inhabited
 
-instance : ToFormat FieldLHS := ⟨fun lhs =>
-  match lhs with
-  | .fieldName _ n  => format n
-  | .fieldIndex _ i => format i
-  | .modifyOp _ i   => "[" ++ i.prettyPrint ++ "]"⟩
+instance : ToFormat FieldLHS where
+  format
+    | .fieldName _ n  => format n
+    | .fieldIndex _ i => format i
+    | .modifyOp _ i   => "[" ++ i.prettyPrint ++ "]"
 
+/--
+`FieldVal StructInstView` is a representation of a field value in the structure instance.
+-/
 inductive FieldVal (σ : Type) where
-  | term  (stx : Syntax) : FieldVal σ
+  /-- A `term` to use for the value of the field. -/
+  | term (stx : Syntax)  : FieldVal σ
+  /-- A `StructInstView` to use for the value of a subobject field. -/
   | nested (s : σ)       : FieldVal σ
-  | default              : FieldVal σ -- mark that field must be synthesized using default value
+  /-- A field that was not provided and should be synthesized using default values. -/
+  | default              : FieldVal σ
   deriving Inhabited
 
+/--
+`Field StructInstView` is a representation of a field in the structure instance.
+-/
 structure Field (σ : Type) where
+  /-- The whole field syntax. -/
   ref   : Syntax
+  /-- The LHS decomposed into components. -/
   lhs   : List FieldLHS
+  /-- The value of the field. -/
   val   : FieldVal σ
+  /-- The elaborated field value, filled in at `elabStruct`.
+  Missing fields use a metavariable for the elaborated value and are later solved for in `DefaultFields.propagate`. -/
   expr? : Option Expr := none
   deriving Inhabited
 
+/--
+Returns if the field has a single component in its LHS.
+-/
 def Field.isSimple {σ} : Field σ → Bool
   | { lhs := [_], .. } => true
   | _                  => false
 
-inductive Struct where
-  /-- Remark: the field `params` is use for default value propagation. It is initially empty, and then set at `elabStruct`. -/
-  | mk (ref : Syntax) (structName : Name) (params : Array (Name × Expr)) (fields : List (Field Struct)) (source : Source)
+/--
+The view for structure instance notation.
+-/
+structure StructInstView where
+  /-- The syntax for the whole structure instance. -/
+  ref : Syntax
+  /-- The name of the structure for the type of the structure instance. -/
+  structName : Name
+  /-- Used for default values, to propagate structure type parameters. It is initially empty, and then set at `elabStruct`. -/
+  params : Array (Name × Expr)
+  /-- The fields of the structure instance. -/
+  fields : List (Field StructInstView)
+  /-- The additional sources for fields for the structure instance. -/
+  sources : SourcesView
   deriving Inhabited
 
-abbrev Fields := List (Field Struct)
-
-def Struct.ref : Struct → Syntax
-  | ⟨ref, _, _, _, _⟩ => ref
-
-def Struct.structName : Struct → Name
-  | ⟨_, structName, _, _, _⟩ => structName
-
-def Struct.params : Struct → Array (Name × Expr)
-  | ⟨_, _, params, _, _⟩ => params
-
-def Struct.fields : Struct → Fields
-  | ⟨_, _, _, fields, _⟩ => fields
-
-def Struct.source : Struct → Source
-  | ⟨_, _, _, _, s⟩ => s
+/-- Abbreviation for the type of `StructInstView.fields`, namely `List (Field StructInstView)`. -/
+abbrev Fields := List (Field StructInstView)
 
 /-- `true` iff all fields of the given structure are marked as `default` -/
-partial def Struct.allDefault (s : Struct) : Bool :=
+partial def StructInstView.allDefault (s : StructInstView) : Bool :=
   s.fields.all fun { val := val,  .. } => match val with
     | .term _   => false
     | .default  => true
     | .nested s => allDefault s
 
-def formatField (formatStruct : Struct → Format) (field : Field Struct) : Format :=
+def formatField (formatStruct : StructInstView → Format) (field : Field StructInstView) : Format :=
   Format.joinSep field.lhs " . " ++ " := " ++
     match field.val with
     | .term v   => v.prettyPrint
     | .nested s => formatStruct s
     | .default  => "<default>"
 
-partial def formatStruct : Struct → Format
+partial def formatStruct : StructInstView → Format
   | ⟨_, _,          _, fields, source⟩ =>
     let fieldsFmt := Format.joinSep (fields.map (formatField formatStruct)) ", "
     let implicitFmt := if source.implicit.isSome then " .. " else ""
@@ -311,31 +378,39 @@ partial def formatStruct : Struct → Format
     else
       "{" ++ format (source.explicit.map (·.stx)) ++ " with " ++ fieldsFmt ++ implicitFmt ++ "}"
 
-instance : ToFormat Struct     := ⟨formatStruct⟩
-instance : ToString Struct := ⟨toString ∘ format⟩
+instance : ToFormat StructInstView     := ⟨formatStruct⟩
+instance : ToString StructInstView := ⟨toString ∘ format⟩
 
-instance : ToFormat (Field Struct) := ⟨formatField formatStruct⟩
-instance : ToString (Field Struct) := ⟨toString ∘ format⟩
+instance : ToFormat (Field StructInstView) := ⟨formatField formatStruct⟩
+instance : ToString (Field StructInstView) := ⟨toString ∘ format⟩
+
+/--
+Converts a `FieldLHS` back into syntax. This assumes the `ref` fields have the correct structure.
 
-/-
 Recall that `structInstField` elements have the form
-```
-   def structInstField  := leading_parser structInstLVal >> " := " >> termParser
-   def structInstLVal   := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (("." >> (ident <|> numLit)) <|> structInstArrayRef)
-   def structInstArrayRef := leading_parser "[" >> termParser >>"]"
+```lean
+def structInstField  := leading_parser structInstLVal >> " := " >> termParser
+def structInstLVal   := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (("." >> (ident <|> numLit)) <|> structInstArrayRef)
+def structInstArrayRef := leading_parser "[" >> termParser >>"]"
 ```
 -/
 -- Remark: this code relies on the fact that `expandStruct` only transforms `fieldLHS.fieldName`
-def FieldLHS.toSyntax (first : Bool) : FieldLHS → Syntax
+private def FieldLHS.toSyntax (first : Bool) : FieldLHS → Syntax
   | .modifyOp   stx _    => stx
   | .fieldName  stx name => if first then mkIdentFrom stx name else mkGroupNode #[mkAtomFrom stx ".", mkIdentFrom stx name]
   | .fieldIndex stx _    => if first then stx else mkGroupNode #[mkAtomFrom stx ".", stx]
 
-def FieldVal.toSyntax : FieldVal Struct → Syntax
+/--
+Converts a `FieldVal StructInstView` back into syntax. Only supports `.term`, and it assumes the `stx` field has the correct structure.
+-/
+private def FieldVal.toSyntax : FieldVal Struct → Syntax
   | .term stx => stx
-  | _                 => unreachable!
+  | _         => unreachable!
 
-def Field.toSyntax : Field Struct → Syntax
+/--
+Converts a `Field StructInstView` back into syntax. Used to construct synthetic structure instance notation for subobjects in `StructInst.expandStruct` processing.
+-/
+private def Field.toSyntax : Field Struct → Syntax
   | field =>
     let stx := field.ref
     let stx := stx.setArg 2 field.val.toSyntax
@@ -343,6 +418,7 @@ def Field.toSyntax : Field Struct → Syntax
     | first::rest => stx.setArg 0 <| mkNullNode #[first.toSyntax true, mkNullNode <| rest.toArray.map (FieldLHS.toSyntax false) ]
     | _ => unreachable!
 
+/-- Creates a view of a field left-hand side. -/
 private def toFieldLHS (stx : Syntax) : MacroM FieldLHS :=
   if stx.getKind == ``Lean.Parser.Term.structInstArrayRef then
     return FieldLHS.modifyOp stx stx[1]
@@ -355,7 +431,12 @@ private def toFieldLHS (stx : Syntax) : MacroM FieldLHS :=
       | some idx => return FieldLHS.fieldIndex stx idx
       | none     => Macro.throwError "unexpected structure syntax"
 
-private def mkStructView (stx : Syntax) (structName : Name) (source : Source) : MacroM Struct := do
+/--
+Creates a structure instance view from structure instance notation
+and the computed structure name (from `Lean.Elab.Term.StructInst.getStructName`)
+and structure source view (from `Lean.Elab.Term.StructInst.getStructSources`).
+-/
+private def mkStructView (stx : Syntax) (structName : Name) (sources : SourcesView) : MacroM StructInstView := do
   /- Recall that `stx` is of the form
      ```
      leading_parser "{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
@@ -371,24 +452,18 @@ private def mkStructView (stx : Syntax) (structName : Name) (source : Source) :
     let val      := fieldStx[2]
     let first    ← toFieldLHS fieldStx[0][0]
     let rest     ← fieldStx[0][1].getArgs.toList.mapM toFieldLHS
-    return { ref := fieldStx, lhs := first :: rest, val := FieldVal.term val : Field Struct }
-  return ⟨stx, structName, #[], fields, source⟩
+    return { ref := fieldStx, lhs := first :: rest, val := FieldVal.term val : Field StructInstView }
+  return { ref := stx, structName, params := #[], fields, sources }
 
-def Struct.modifyFieldsM {m : Type → Type} [Monad m] (s : Struct) (f : Fields → m Fields) : m Struct :=
+def StructInstView.modifyFieldsM {m : Type → Type} [Monad m] (s : StructInstView) (f : Fields → m Fields) : m StructInstView :=
   match s with
-  | ⟨ref, structName, params, fields, source⟩ => return ⟨ref, structName, params, (← f fields), source⟩
+  | { ref, structName, params, fields, sources } => return { ref, structName, params, fields := (← f fields), sources }
 
-def Struct.modifyFields (s : Struct) (f : Fields → Fields) : Struct :=
+def StructInstView.modifyFields (s : StructInstView) (f : Fields → Fields) : StructInstView :=
   Id.run <| s.modifyFieldsM f
 
-def Struct.setFields (s : Struct) (fields : Fields) : Struct :=
-  s.modifyFields fun _ => fields
-
-def Struct.setParams (s : Struct) (ps : Array (Name × Expr)) : Struct :=
-  match s with
-  | ⟨ref, structName, _, fields, source⟩ => ⟨ref, structName, ps, fields, source⟩
-
-private def expandCompositeFields (s : Struct) : Struct :=
+/-- Expands name field LHSs with multi-component names into multi-component LHSs. -/
+private def expandCompositeFields (s : StructInstView) : StructInstView :=
   s.modifyFields fun fields => fields.map fun field => match field with
     | { lhs := .fieldName _ (.str Name.anonymous ..) :: _, .. } => field
     | { lhs := .fieldName ref n@(.str ..) :: rest, .. } =>
@@ -396,7 +471,8 @@ private def expandCompositeFields (s : Struct) : Struct :=
       { field with lhs := newEntries ++ rest }
     | _ => field
 
-private def expandNumLitFields (s : Struct) : TermElabM Struct :=
+/-- Replaces numeric index field LHSs with the corresponding named field, or throws an error if no such field exists. -/
+private def expandNumLitFields (s : StructInstView) : TermElabM StructInstView :=
   s.modifyFieldsM fun fields => do
     let env ← getEnv
     let fieldNames := getStructureFields env s.structName
@@ -407,28 +483,31 @@ private def expandNumLitFields (s : Struct) : TermElabM Struct :=
         else return { field with lhs := .fieldName ref fieldNames[idx - 1]! :: rest }
       | _ => return field
 
-/-- For example, consider the following structures:
-   ```
-   structure A where
-     x : Nat
+/--
+Expands fields that are actually represented as fields of subobject fields.
 
-   structure B extends A where
-     y : Nat
+For example, consider the following structures:
+```
+structure A where
+  x : Nat
 
-   structure C extends B where
-     z : Bool
-   ```
-   This method expands parent structure fields using the path to the parent structure.
-   For example,
-   ```
-   { x := 0, y := 0, z := true : C }
-   ```
-   is expanded into
-   ```
-   { toB.toA.x := 0, toB.y := 0, z := true : C }
-   ```
+structure B extends A where
+  y : Nat
+
+structure C extends B where
+  z : Bool
+```
+This method expands parent structure fields using the path to the parent structure.
+For example,
+```
+{ x := 0, y := 0, z := true : C }
+```
+is expanded into
+```
+{ toB.toA.x := 0, toB.y := 0, z := true : C }
+```
 -/
-private def expandParentFields (s : Struct) : TermElabM Struct := do
+private def expandParentFields (s : StructInstView) : TermElabM StructInstView := do
   let env ← getEnv
   s.modifyFieldsM fun fields => fields.mapM fun field => do match field with
     | { lhs := .fieldName ref fieldName :: _,    .. } =>
@@ -448,6 +527,11 @@ private def expandParentFields (s : Struct) : TermElabM Struct := do
 
 private abbrev FieldMap := Std.HashMap Name Fields
 
+/--
+Creates a hash map collecting all fields with the same first name component.
+Throws an error if there are multiple simple fields with the same name.
+Used by `StructInst.expandStruct` processing.
+-/
 private def mkFieldMap (fields : Fields) : TermElabM FieldMap :=
   fields.foldlM (init := {}) fun fieldMap field =>
     match field.lhs with
@@ -461,15 +545,16 @@ private def mkFieldMap (fields : Fields) : TermElabM FieldMap :=
       | _ => return fieldMap.insert fieldName [field]
     | _ => unreachable!
 
-private def isSimpleField? : Fields → Option (Field Struct)
+/--
+Given a value of the hash map created by `mkFieldMap`, returns true if the value corresponds to a simple field.
+-/
+private def isSimpleField? : Fields → Option (Field StructInstView)
   | [field] => if field.isSimple then some field else none
   | _       => none
 
-private def getFieldIdx (structName : Name) (fieldNames : Array Name) (fieldName : Name) : TermElabM Nat := do
-  match fieldNames.findIdx? fun n => n == fieldName with
-  | some idx => return idx
-  | none     => throwError "field '{fieldName}' is not a valid field of '{structName}'"
-
+/--
+Creates projection notation for the given structure field. Used
+-/
 def mkProjStx? (s : Syntax) (structName : Name) (fieldName : Name) : TermElabM (Option Syntax) := do
   if (findField? (← getEnv) structName fieldName).isNone then
     return none
@@ -478,7 +563,10 @@ def mkProjStx? (s : Syntax) (structName : Name) (fieldName : Name) : TermElabM (
       #[mkAtomFrom s "@",
         mkNode ``Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName]]
 
-def findField? (fields : Fields) (fieldName : Name) : Option (Field Struct) :=
+/--
+Finds a simple field of the given name.
+-/
+def findField? (fields : Fields) (fieldName : Name) : Option (Field StructInstView) :=
   fields.find? fun field =>
     match field.lhs with
     | [.fieldName _ n] => n == fieldName
@@ -486,7 +574,10 @@ def findField? (fields : Fields) (fieldName : Name) : Option (Field Struct) :=
 
 mutual
 
-  private partial def groupFields (s : Struct) : TermElabM Struct := do
+  /--
+  Groups compound fields according to which subobject they are from.
+  -/
+  private partial def groupFields (s : StructInstView) : TermElabM StructInstView := do
     let env ← getEnv
     withRef s.ref do
     s.modifyFieldsM fun fields => do
@@ -499,14 +590,14 @@ mutual
           let field := fields.head!
           match Lean.isSubobjectField? env s.structName fieldName with
           | some substructName =>
-            let substruct := Struct.mk s.ref substructName #[] substructFields s.source
+            let substruct := { ref := s.ref, structName := substructName, params := #[], fields := substructFields, sources := s.sources }
             let substruct ← expandStruct substruct
             pure { field with lhs := [field.lhs.head!], val := FieldVal.nested substruct }
           | none =>
             let updateSource (structStx : Syntax) : TermElabM Syntax := do
-              let sourcesNew ← s.source.explicit.filterMapM fun source => mkProjStx? source.stx source.structName fieldName
+              let sourcesNew ← s.sources.explicit.filterMapM fun source => mkProjStx? source.stx source.structName fieldName
               let explicitSourceStx := if sourcesNew.isEmpty then mkNullNode else mkSourcesWithSyntax sourcesNew
-              let implicitSourceStx := s.source.implicit.getD mkNullNode
+              let implicitSourceStx := s.sources.implicit.getD mkNullNode
               return (structStx.setArg 1 explicitSourceStx).setArg 3 implicitSourceStx
             let valStx := s.ref -- construct substructure syntax using s.ref as template
             let valStx := valStx.setArg 4 mkNullNode -- erase optional expected type
@@ -518,7 +609,7 @@ mutual
   Adds in the missing fields using the explicit sources.
   Invariant: a missing field always comes from the first source that can provide it.
   -/
-  private partial def addMissingFields (s : Struct) : TermElabM Struct := do
+  private partial def addMissingFields (s : StructInstView) : TermElabM StructInstView := do
     let env ← getEnv
     let fieldNames := getStructureFields env s.structName
     let ref := s.ref.mkSynthetic
@@ -527,7 +618,7 @@ mutual
         match findField? s.fields fieldName with
         | some field => return field::fields
         | none       =>
-          let addField (val : FieldVal Struct) : TermElabM Fields := do
+          let addField (val : FieldVal StructInstView) : TermElabM Fields := do
             return { ref, lhs := [FieldLHS.fieldName ref fieldName], val := val } :: fields
           match Lean.isSubobjectField? env s.structName fieldName with
           | some substructName =>
@@ -535,8 +626,8 @@ mutual
             let downFields := getStructureFieldsFlattened env substructName false
             -- Filter out all explicit sources that do not share a leaf field keeping
             -- structure with no fields
-            let filtered := s.source.explicit.filter fun source =>
-              let sourceFields := getStructureFieldsFlattened env source.structName false
+            let filtered := s.sources.explicit.filter fun sources =>
+              let sourceFields := getStructureFieldsFlattened env sources.structName false
               sourceFields.any (fun name => downFields.contains name) || sourceFields.isEmpty
             -- Take the first such one remaining
             match filtered[0]? with
@@ -550,27 +641,30 @@ mutual
               -- No sources could provide this subobject in the proper order.
               -- Recurse to handle default values for fields.
               else
-                let substruct := Struct.mk ref substructName #[] [] s.source
+                let substruct := { ref, structName := substructName, params := #[], fields := [], sources := s.sources }
                 let substruct ← expandStruct substruct
                 addField (FieldVal.nested substruct)
             -- No sources could provide this subobject.
             -- Recurse to handle default values for fields.
             | none =>
-              let substruct := Struct.mk ref substructName #[] [] s.source
+              let substruct := { ref, structName := substructName, params := #[], fields := [], sources := s.sources }
               let substruct ← expandStruct substruct
               addField (FieldVal.nested substruct)
           -- Since this is not a subobject field, we are free to use the first source that can
             -- provide it.
           | none =>
-            if let some val ← s.source.explicit.findSomeM? fun source => mkProjStx? source.stx source.structName fieldName then
+            if let some val ← s.sources.explicit.findSomeM? fun source => mkProjStx? source.stx source.structName fieldName then
               addField (FieldVal.term val)
-            else if s.source.implicit.isSome then
+            else if s.sources.implicit.isSome then
               addField (FieldVal.term (mkHole ref))
             else
               addField FieldVal.default
-      return s.setFields fields.reverse
+      return { s with fields := fields.reverse }
 
-  private partial def expandStruct (s : Struct) : TermElabM Struct := do
+  /--
+  Expands all fields of the structure instance, consolidates compound fields into subobject fields, and adds missing fields.
+  -/
+  private partial def expandStruct (s : StructInstView) : TermElabM StructInstView := do
     let s := expandCompositeFields s
     let s ← expandNumLitFields s
     let s ← expandParentFields s
@@ -579,10 +673,17 @@ mutual
 
 end
 
+/--
+The constructor to use for the structure instance notation.
+-/
 structure CtorHeaderResult where
+  /-- The constructor function with applied structure parameters. -/
   ctorFn     : Expr
+  /-- The type of `ctorFn` -/
   ctorFnType : Expr
+  /-- Instance metavariables for structure parameters that are instance implicit. -/
   instMVars  : Array MVarId
+  /-- Type parameter names and metavariables for each parameter. Used to seed `StructInstView.params`. -/
   params     : Array (Name × Expr)
 
 private def mkCtorHeaderAux : Nat → Expr → Expr → Array MVarId → Array (Name × Expr) → TermElabM CtorHeaderResult
@@ -604,6 +705,7 @@ private partial def getForallBody : Nat → Expr → Option Expr
   | _+1, _                => none
   | 0,   type             => type
 
+/-- Attempts to use the expected type to solve for structure parameters. -/
 private def propagateExpectedType (type : Expr) (numFields : Nat) (expectedType? : Option Expr) : TermElabM Unit := do
   match expectedType? with
   | none              => return ()
@@ -614,6 +716,7 @@ private def propagateExpectedType (type : Expr) (numFields : Nat) (expectedType?
         unless typeBody.hasLooseBVars do
           discard <| isDefEq expectedType typeBody
 
+/-- Elaborates the structure constructor using the expected type, filling in all structure parameters. -/
 private def mkCtorHeader (ctorVal : ConstructorVal) (expectedType? : Option Expr) : TermElabM CtorHeaderResult := do
   let us ← mkFreshLevelMVars ctorVal.levelParams.length
   let val  := Lean.mkConst ctorVal.name us
@@ -623,32 +726,43 @@ private def mkCtorHeader (ctorVal : ConstructorVal) (expectedType? : Option Expr
   synthesizeAppInstMVars r.instMVars r.ctorFn
   return r
 
+/-- Annotates an expression that it is a value for a missing field. -/
 def markDefaultMissing (e : Expr) : Expr :=
   mkAnnotation `structInstDefault e
 
+/-- If the expression has been annotated by `markDefaultMissing`, returns the unannotated expression. -/
 def defaultMissing? (e : Expr) : Option Expr :=
   annotation? `structInstDefault e
 
+/-- Throws "failed to elaborate field" error. -/
 def throwFailedToElabField {α} (fieldName : Name) (structName : Name) (msgData : MessageData) : TermElabM α :=
   throwError "failed to elaborate field '{fieldName}' of '{structName}, {msgData}"
 
-def trySynthStructInstance? (s : Struct) (expectedType : Expr) : TermElabM (Option Expr) := do
+/-- If the struct has all-missing fields, tries to synthesize the structure using typeclass inference. -/
+def trySynthStructInstance? (s : StructInstView) (expectedType : Expr) : TermElabM (Option Expr) := do
   if !s.allDefault then
     return none
   else
     try synthInstance? expectedType catch _ => return none
 
+/-- The result of elaborating a `StructInstView` structure instance view. -/
 structure ElabStructResult where
+  /-- The elaborated value. -/
   val       : Expr
-  struct    : Struct
+  /-- The modified `StructInstView` view after elaboration. -/
+  struct    : StructInstView
+  /-- Metavariables for instance implicit fields. These will be registered after default value propagation. -/
   instMVars : Array MVarId
 
-private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : TermElabM ElabStructResult := withRef s.ref do
+/--
+Main elaborator for structure instances.
+-/
+private partial def elabStructInstView (s : StructInstView) (expectedType? : Option Expr) : TermElabM ElabStructResult := withRef s.ref do
   let env ← getEnv
   let ctorVal := getStructureCtor env s.structName
   if isPrivateNameFromImportedModule env ctorVal.name then
     throwError "invalid \{...} notation, constructor for `{s.structName}` is marked as private"
-  -- We store the parameters at the resulting `Struct`. We use this information during default value propagation.
+  -- We store the parameters at the resulting `StructInstView`. We use this information during default value propagation.
   let { ctorFn, ctorFnType, params, .. } ← mkCtorHeader ctorVal expectedType?
   let (e, _, fields, instMVars) ← s.fields.foldlM (init := (ctorFn, ctorFnType, [], #[])) fun (e, type, fields, instMVars) field => do
     match field.lhs with
@@ -657,7 +771,7 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
       trace[Elab.struct] "elabStruct {field}, {type}"
       match type with
       | .forallE _ d b bi =>
-        let cont (val : Expr) (field : Field Struct) (instMVars := instMVars) : TermElabM (Expr × Expr × Fields × Array MVarId) := do
+        let cont (val : Expr) (field : Field StructInstView) (instMVars := instMVars) : TermElabM (Expr × Expr × Fields × Array MVarId) := do
           pushInfoTree <| InfoTree.node (children := {}) <| Info.ofFieldInfo {
             projName := s.structName.append fieldName, fieldName, lctx := (← getLCtx), val, stx := ref }
           let e     := mkApp e val
@@ -671,7 +785,7 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
           match (← trySynthStructInstance? s d) with
           | some val => cont val { field with val := FieldVal.term (mkHole field.ref) }
           | none     =>
-            let { val, struct := sNew, instMVars := instMVarsNew } ← elabStruct s (some d)
+            let { val, struct := sNew, instMVars := instMVarsNew } ← elabStructInstView s (some d)
             let val ← ensureHasType d val
             cont val { field with val := FieldVal.nested sNew } (instMVars ++ instMVarsNew)
         | .default  =>
@@ -700,17 +814,21 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
               cont (markDefaultMissing val) field
       | _ => withRef field.ref <| throwFailedToElabField fieldName s.structName m!"unexpected constructor type{indentExpr type}"
     | _ => throwErrorAt field.ref "unexpected unexpanded structure field"
-  return { val := e, struct := s.setFields fields.reverse |>.setParams params, instMVars }
+  return { val := e, struct := { s with fields := fields.reverse, params }, instMVars }
 
 namespace DefaultFields
 
+/--
+Context for default value propagation.
+-/
 structure Context where
-  -- We must search for default values overridden in derived structures
-  structs : Array Struct := #[]
+  /-- The current path through `.nested` subobject structures. We must search for default values overridden in derived structures. -/
+  structs : Array StructInstView := #[]
+  /-- The collection of structures that could provide a default value. -/
   allStructNames : Array Name := #[]
   /--
   Consider the following example:
-  ```
+  ```lean
   structure A where
     x : Nat := 1
 
@@ -736,22 +854,29 @@ structure Context where
   -/
   maxDistance : Nat := 0
 
+/--
+State for default value propagation
+-/
 structure State where
+  /-- Whether progress has been made so far on this round of the propagation loop. -/
   progress : Bool := false
 
-partial def collectStructNames (struct : Struct) (names : Array Name) : Array Name :=
+/-- Collects all structures that may provide default values for fields. -/
+partial def collectStructNames (struct : StructInstView) (names : Array Name) : Array Name :=
   let names := names.push struct.structName
   struct.fields.foldl (init := names) fun names field =>
     match field.val with
     | .nested struct => collectStructNames struct names
     | _ => names
 
-partial def getHierarchyDepth (struct : Struct) : Nat :=
+/-- Gets the maximum nesting depth of subobjects. -/
+partial def getHierarchyDepth (struct : StructInstView) : Nat :=
   struct.fields.foldl (init := 0) fun max field =>
     match field.val with
     | .nested struct => Nat.max max (getHierarchyDepth struct + 1)
     | _ => max
 
+/-- Returns whether the field is still missing. -/
 def isDefaultMissing? [Monad m] [MonadMCtx m] (field : Field Struct) : m Bool := do
   if let some expr := field.expr? then
     if let some (.mvar mvarId) := defaultMissing? expr then
@@ -759,40 +884,51 @@ def isDefaultMissing? [Monad m] [MonadMCtx m] (field : Field Struct) : m Bool :=
         return true
   return false
 
-partial def findDefaultMissing? [Monad m] [MonadMCtx m] (struct : Struct) : m (Option (Field Struct)) :=
+/-- Returns a field that is still missing. -/
+partial def findDefaultMissing? [Monad m] [MonadMCtx m] (struct : StructInstView) : m (Option (Field StructInstView)) :=
   struct.fields.findSomeM? fun field => do
    match field.val with
    | .nested struct => findDefaultMissing? struct
    | _ => return if (← isDefaultMissing? field) then field else none
 
-partial def allDefaultMissing [Monad m] [MonadMCtx m] (struct : Struct) : m (Array (Field Struct)) :=
+/-- Returns all fields that are still missing. -/
+partial def allDefaultMissing [Monad m] [MonadMCtx m] (struct : StructInstView) : m (Array (Field StructInstView)) :=
   go struct *> get |>.run' #[]
 where
-  go (struct : Struct) : StateT (Array (Field Struct)) m Unit :=
+  go (struct : StructInstView) : StateT (Array (Field StructInstView)) m Unit :=
     for field in struct.fields do
       if let .nested struct := field.val then
         go struct
       else if (← isDefaultMissing? field) then
         modify (·.push field)
 
-def getFieldName (field : Field Struct) : Name :=
+/-- Returns the name of the field. Assumes all fields under consideration are simple and named. -/
+def getFieldName (field : Field StructInstView) : Name :=
   match field.lhs with
   | [.fieldName _ fieldName] => fieldName
   | _ => unreachable!
 
 abbrev M := ReaderT Context (StateRefT State TermElabM)
 
+/-- Returns whether we should interrupt the round because we have made progress allowing nonzero depth. -/
 def isRoundDone : M Bool := do
   return (← get).progress && (← read).maxDistance > 0
 
-def getFieldValue? (struct : Struct) (fieldName : Name) : Option Expr :=
+/-- Returns the `expr?` for the given field. -/
+def getFieldValue? (struct : StructInstView) (fieldName : Name) : Option Expr :=
   struct.fields.findSome? fun field =>
     if getFieldName field == fieldName then
       field.expr?
     else
       none
 
-partial def mkDefaultValueAux? (struct : Struct) : Expr → TermElabM (Option Expr)
+/-- Instantiates a default value from the given default value declaration, if applicable. -/
+partial def mkDefaultValue? (struct : StructInstView) (cinfo : ConstantInfo) : TermElabM (Option Expr) :=
+  withRef struct.ref do
+  let us ← mkFreshLevelMVarsFor cinfo
+  process (← instantiateValueLevelParams cinfo us)
+where
+  process : Expr → TermElabM (Option Expr)
   | .lam n d b c => withRef struct.ref do
     if c.isExplicit then
       let fieldName := n
@@ -801,29 +937,26 @@ partial def mkDefaultValueAux? (struct : Struct) : Expr → TermElabM (Option Ex
       | some val =>
         let valType ← inferType val
         if (← isDefEq valType d) then
-          mkDefaultValueAux? struct (b.instantiate1 val)
+          process (b.instantiate1 val)
         else
           return none
     else
       if let some (_, param) := struct.params.find? fun (paramName, _) => paramName == n then
         -- Recall that we did not use to have support for parameter propagation here.
         if (← isDefEq (← inferType param) d) then
-          mkDefaultValueAux? struct (b.instantiate1 param)
+          process (b.instantiate1 param)
         else
           return none
       else
         let arg ← mkFreshExprMVar d
-        mkDefaultValueAux? struct (b.instantiate1 arg)
+        process (b.instantiate1 arg)
   | e =>
     let_expr id _ a := e | return some e
     return some a
 
-def mkDefaultValue? (struct : Struct) (cinfo : ConstantInfo) : TermElabM (Option Expr) :=
-  withRef struct.ref do
-  let us ← mkFreshLevelMVarsFor cinfo
-  mkDefaultValueAux? struct (← instantiateValueLevelParams cinfo us)
-
-/-- Reduce default value. It performs beta reduction and projections of the given structures. -/
+/--
+Reduces a default value. It performs beta reduction and projections of the given structures to reduce them to the provided values for fields.
+-/
 partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
   match e with
   | .forallE ..   =>
@@ -880,7 +1013,10 @@ where
     else
       k
 
-partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Array Name) (maxDistance : Nat) (fieldName : Name) (mvarId : MVarId) : TermElabM Bool :=
+/--
+Attempts to synthesize a default value for a missing field `fieldName` using default values from each structure in `structs`.
+-/
+def tryToSynthesizeDefault (structs : Array StructInstView) (allStructNames : Array Name) (maxDistance : Nat) (fieldName : Name) (mvarId : MVarId) : TermElabM Bool :=
   let rec loop (i : Nat) (dist : Nat) := do
     if dist > maxDistance then
       return false
@@ -900,14 +1036,25 @@ partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Ar
           | none   =>
             let mvarDecl ← getMVarDecl mvarId
             let val ← ensureHasType mvarDecl.type val
-            mvarId.assign val
-            return true
+            /-
+            We must use `checkedAssign` here to ensure we do not create a cyclic
+            assignment. See #3150.
+            This can happen when there are holes in the the fields the default value
+            depends on.
+            Possible improvement: create a new `_` instead of returning `false` when
+            `checkedAssign` fails. Reason: the field will not be needed after the
+            other `_` are resolved by the user.
+            -/
+            mvarId.checkedAssign val
       | _ => loop (i+1) dist
     else
       return false
   loop 0 0
 
-partial def step (struct : Struct) : M Unit :=
+/--
+Performs one step of default value synthesis.
+-/
+partial def step (struct : StructInstView) : M Unit :=
   unless (← isRoundDone) do
     withReader (fun ctx => { ctx with structs := ctx.structs.push struct }) do
       for field in struct.fields do
@@ -924,7 +1071,10 @@ partial def step (struct : Struct) : M Unit :=
                   modify fun _ => { progress := true }
             | _ => pure ()
 
-partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : Struct) : M Unit := do
+/--
+Main entry point to default value synthesis in the `M` monad.
+-/
+partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : StructInstView) : M Unit := do
   match (← findDefaultMissing? struct) with
   | none       => return () -- Done
   | some field =>
@@ -947,16 +1097,22 @@ partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : Struct) : M
       else
         propagateLoop hierarchyDepth (d+1) struct
 
-def propagate (struct : Struct) : TermElabM Unit :=
+/--
+Synthesizes default values for all missing fields, if possible.
+-/
+def propagate (struct : StructInstView) : TermElabM Unit :=
   let hierarchyDepth := getHierarchyDepth struct
   let structNames := collectStructNames struct #[]
   propagateLoop hierarchyDepth 0 struct { allStructNames := structNames } |>.run' {}
 
 end DefaultFields
 
-private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (source : Source) : TermElabM Expr := do
-  let structName ← getStructName expectedType? source
-  let struct ← liftMacroM <| mkStructView stx structName source
+/--
+Main entry point to elaborator for structure instance notation, unless the structure instance is a modifyOp.
+-/
+private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sources : SourcesView) : TermElabM Expr := do
+  let structName ← getStructName expectedType? sources
+  let struct ← liftMacroM <| mkStructView stx structName sources
   let struct ← expandStruct struct
   trace[Elab.struct] "{struct}"
   /- We try to synthesize pending problems with `withSynthesize` combinator before trying to use default values.
@@ -974,7 +1130,7 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour
 
      TODO: investigate whether this design decision may have unintended side effects or produce confusing behavior.
   -/
-  let { val := r, struct, instMVars } ← withSynthesize (postpone := .yes) <| elabStruct struct expectedType?
+  let { val := r, struct, instMVars } ← withSynthesize (postpone := .yes) <| elabStructInstView struct expectedType?
   trace[Elab.struct] "before propagate {r}"
   DefaultFields.propagate struct
   synthesizeAppInstMVars instMVars r
@@ -984,13 +1140,13 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour
   match (← expandNonAtomicExplicitSources stx) with
   | some stxNew => withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
   | none =>
-    let sourceView ← getStructSource stx
+    let sourcesView ← getStructSources stx
     if let some modifyOp ← isModifyOp? stx then
-      if sourceView.explicit.isEmpty then
+      if sourcesView.explicit.isEmpty then
         throwError "invalid \{...} notation, explicit source is required when using '[<index>] := <value>'"
-      elabModifyOp stx modifyOp sourceView.explicit expectedType?
+      elabModifyOp stx modifyOp sourcesView.explicit expectedType?
     else
-      elabStructInstAux stx expectedType? sourceView
+      elabStructInstAux stx expectedType? sourcesView
 
 builtin_initialize
   registerTraceClass `Elab.struct

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/Change.lean

@@ -13,6 +13,31 @@ open Meta
 # Implementation of the `change` tactic
 -/
 
+/--
+Elaborates the pattern `p` and ensures that it is defeq to `e`.
+Emulates `(show p from ?m : e)`, returning the type of `?m`, but `e` and `p` do not need to be types.
+Unlike `(show p from ?m : e)`, this can assign synthetic opaque metavariables appearing in `p`.
+-/
+def elabChange (e : Expr) (p : Term) : TacticM Expr := do
+  let p ← runTermElab do
+    let p ← Term.elabTermEnsuringType p (← inferType e)
+    unless ← isDefEq p e do
+      /-
+      Sometimes isDefEq can fail due to postponed elaboration problems.
+      We synthesize pending synthetic mvars while allowing typeclass instances to be postponed,
+      which might enable solving for them with an additional `isDefEq`.
+      -/
+      Term.synthesizeSyntheticMVars (postpone := .partial)
+      discard <| isDefEq p e
+    pure p
+  withAssignableSyntheticOpaque do
+    unless ← isDefEq p e do
+      let (p, tgt) ← addPPExplicitToExposeDiff p e
+      throwError "\
+        'change' tactic failed, pattern{indentExpr p}\n\
+        is not definitionally equal to target{indentExpr tgt}"
+    instantiateMVars p
+
 /-- `change` can be used to replace the main goal or its hypotheses with
 different, yet definitionally equal, goal or hypotheses.
 
@@ -38,15 +63,13 @@ the main goal. -/
   | `(tactic| change $newType:term $[$loc:location]?) => do
     withLocation (expandOptLocation (Lean.mkOptionalNode loc))
       (atLocal := fun h => do
-        let hTy ← h.getType
-        -- This is a hack to get the new type to elaborate in the same sort of way that
-        -- it would for a `show` expression for the goal.
-        let mvar ← mkFreshExprMVar none
-        let (_, mvars) ← elabTermWithHoles
-                          (← `(term | show $newType from $(← Term.exprToSyntax mvar))) hTy `change
+        let (hTy', mvars) ← withCollectingNewGoalsFrom (elabChange (← h.getType) newType) (← getMainTag) `change
         liftMetaTactic fun mvarId => do
-          return (← mvarId.changeLocalDecl h (← inferType mvar)) :: mvars)
-      (atTarget := evalTactic <| ← `(tactic| refine_lift show $newType from ?_))
-      (failed := fun _ => throwError "change tactic failed")
+          return (← mvarId.changeLocalDecl h hTy') :: mvars)
+      (atTarget := do
+        let (tgt', mvars) ← withCollectingNewGoalsFrom (elabChange (← getMainTarget) newType) (← getMainTag) `change
+        liftMetaTactic fun mvarId => do
+          return (← mvarId.replaceTargetDefEq tgt') :: mvars)
+      (failed := fun _ => throwError "'change' tactic failed")
 
 end Lean.Elab.Tactic

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

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Elab.Tactic.ElabTerm
+import Lean.Elab.Tactic.Change
 import Lean.Elab.Tactic.Conv.Basic
 
 namespace Lean.Elab.Tactic.Conv
@@ -15,11 +16,9 @@ open Meta
   | `(conv| change $e) => withMainContext do
     let lhs ← getLhs
     let mvarCounterSaved := (← getMCtx).mvarCounter
-    let r ← elabTermEnsuringType e (← inferType lhs)
-    logUnassignedAndAbort (← filterOldMVars (← getMVars r) mvarCounterSaved)
-    unless (← isDefEqGuarded r lhs) do
-      throwError "invalid 'change' conv tactic, term{indentExpr r}\nis not definitionally equal to current left-hand-side{indentExpr lhs}"
-    changeLhs r
+    let lhs' ← elabChange lhs e
+    logUnassignedAndAbort (← filterOldMVars (← getMVars lhs') mvarCounterSaved)
+    changeLhs lhs'
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/DiscrTreeKey.lean

@@ -18,21 +18,22 @@ private def mkKey (e : Expr) (simp : Bool) : MetaM (Array Key) := do
   let (_, _, type) ← withReducible <| forallMetaTelescopeReducing e
   let type ← whnfR type
   if simp then
-    if let some (_, lhs, _) := type.eq? then
-      mkPath lhs simpDtConfig
-    else if let some (lhs, _) := type.iff? then
-      mkPath lhs simpDtConfig
-    else if let some (_, lhs, _) := type.ne? then
-      mkPath lhs simpDtConfig
-    else if let some p := type.not? then
-      match p.eq? with
-      | some (_, lhs, _) =>
-        mkPath lhs simpDtConfig
-      | _ => mkPath p simpDtConfig
-    else
-      mkPath type simpDtConfig
+    withSimpGlobalConfig do
+      if let some (_, lhs, _) := type.eq? then
+        mkPath lhs
+      else if let some (lhs, _) := type.iff? then
+        mkPath lhs
+      else if let some (_, lhs, _) := type.ne? then
+        mkPath lhs
+      else if let some p := type.not? then
+        match p.eq? with
+        | some (_, lhs, _) =>
+          mkPath lhs
+        | _ => mkPath p
+      else
+        mkPath type
   else
-    mkPath type {}
+    mkPath type
 
 private def getType (t : TSyntax `term) : TermElabM Expr := do
   if let `($id:ident) := t then

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -542,11 +542,6 @@ declare_config_elab elabDecideConfig Parser.Tactic.DecideConfig
   let cfg ← elabDecideConfig stx[1]
   evalDecideCore `decide cfg
 
-@[builtin_tactic Lean.Parser.Tactic.decideBang] def evalDecideBang : Tactic := fun stx => do
-  let cfg ← elabDecideConfig stx[1]
-  let cfg := { cfg with kernel := true }
-  evalDecideCore `decide! cfg
-
 @[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun stx => do
   let cfg ← elabDecideConfig stx[1]
   let cfg := { cfg with native := true }

src/Lean/Elab/Tactic/Ext.lean

@@ -195,9 +195,6 @@ structure ExtTheorems where
   erased  : PHashSet Name := {}
   deriving Inhabited
 
-/-- Discrimation tree settings for the `ext` extension. -/
-def extExt.config : WhnfCoreConfig := {}
-
 /-- The environment extension to track `@[ext]` theorems. -/
 builtin_initialize extExtension :
     SimpleScopedEnvExtension ExtTheorem ExtTheorems ←
@@ -211,7 +208,7 @@ builtin_initialize extExtension :
 ordered from high priority to low. -/
 @[inline] def getExtTheorems (ty : Expr) : MetaM (Array ExtTheorem) := do
   let extTheorems := extExtension.getState (← getEnv)
-  let arr ← extTheorems.tree.getMatch ty extExt.config
+  let arr ← extTheorems.tree.getMatch ty
   let erasedArr := arr.filter fun thm => !extTheorems.erased.contains thm.declName
   -- Using insertion sort because it is stable and the list of matches should be mostly sorted.
   -- Most ext theorems have default priority.
@@ -258,7 +255,7 @@ builtin_initialize registerBuiltinAttribute {
       but this theorem proves{indentD declTy}"
     let some (ty, lhs, rhs) := declTy.eq? | failNotEq
     unless lhs.isMVar && rhs.isMVar do failNotEq
-    let keys ← withReducible <| DiscrTree.mkPath ty extExt.config
+    let keys ← withReducible <| DiscrTree.mkPath ty
     let priority ← liftCommandElabM <| Elab.liftMacroM do evalPrio (prio.getD (← `(prio| default)))
     extExtension.add {declName, keys, priority} kind
     -- Realize iff theorem

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/Tactic/Simp.lean

@@ -91,7 +91,7 @@ def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TacticM Meta.Simp.Co
   | .simpAll => return (← elabSimpConfigCtxCore optConfig).toConfig
   | .dsimp   => return { (← elabDSimpConfigCore optConfig) with }
 
-private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Expr) (post : Bool) (inv : Bool) (kind : SimpKind) : MetaM SimpTheorems := do
+private def addDeclToUnfoldOrTheorem (config : Meta.ConfigWithKey) (thms : SimpTheorems) (id : Origin) (e : Expr) (post : Bool) (inv : Bool) (kind : SimpKind) : MetaM SimpTheorems := do
   if e.isConst then
     let declName := e.constName!
     let info ← getConstInfo declName
@@ -108,7 +108,7 @@ private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Ex
     let fvarId := e.fvarId!
     let decl ← fvarId.getDecl
     if (← isProp decl.type) then
-      thms.add id #[] e (post := post) (inv := inv)
+      thms.add id #[] e (post := post) (inv := inv) (config := config)
     else if !decl.isLet then
       throwError "invalid argument, variable is not a proposition or let-declaration"
     else if inv then
@@ -116,9 +116,9 @@ private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Ex
     else
       return thms.addLetDeclToUnfold fvarId
   else
-    thms.add id #[] e (post := post) (inv := inv)
+    thms.add id #[] e (post := post) (inv := inv) (config := config)
 
-private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (post : Bool) (inv : Bool) : TermElabM SimpTheorems := do
+private def addSimpTheorem (config : Meta.ConfigWithKey) (thms : SimpTheorems) (id : Origin) (stx : Syntax) (post : Bool) (inv : Bool) : TermElabM SimpTheorems := do
   let thm? ← Term.withoutModifyingElabMetaStateWithInfo <| withRef stx do
     let e ← Term.elabTerm stx none
     Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
@@ -132,7 +132,7 @@ private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (p
     else
       return some (#[], e)
   if let some (levelParams, proof) := thm? then
-    thms.add id levelParams proof (post := post) (inv := inv)
+    thms.add id levelParams proof (post := post) (inv := inv) (config := config)
   else
     return thms
 
@@ -212,7 +212,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             match (← resolveSimpIdTheorem? term) with
             | .expr e  =>
               let name ← mkFreshId
-              thms ← addDeclToUnfoldOrTheorem thms (.stx name arg) e post inv kind
+              thms ← addDeclToUnfoldOrTheorem ctx.indexConfig thms (.stx name arg) e post inv kind
             | .simproc declName =>
               simprocs ← simprocs.add declName post
             | .ext (some ext₁) (some ext₂) _ =>
@@ -224,7 +224,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
               simprocs  := simprocs.push (← ext₂.getSimprocs)
             | .none    =>
               let name ← mkFreshId
-              thms ← addSimpTheorem thms (.stx name arg) term post inv
+              thms ← addSimpTheorem ctx.indexConfig thms (.stx name arg) term post inv
           else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
             starArg := true
           else
@@ -329,7 +329,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
     let hs ← getPropHyps
     for h in hs do
       unless simpTheorems.isErased (.fvar h) do
-        simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr
+        simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr (config := ctx.indexConfig)
     let ctx := ctx.setSimpTheorems simpTheorems
     return { ctx, simprocs, dischargeWrapper }
 

src/Lean/Elab/Tactic/Simproc.lean

@@ -25,7 +25,7 @@ def elabSimprocPattern (stx : Syntax) : MetaM Expr := do
 
 def elabSimprocKeys (stx : Syntax) : MetaM (Array Meta.SimpTheoremKey) := do
   let pattern ← elabSimprocPattern stx
-  DiscrTree.mkPath pattern simpDtConfig
+  withSimpGlobalConfig <| DiscrTree.mkPath pattern
 
 def checkSimprocType (declName : Name) : CoreM Bool := do
   let decl ← getConstInfo declName

src/Lean/Meta/ACLt.lean

@@ -32,6 +32,9 @@ inductive ReduceMode where
   | reduceSimpleOnly
   | none
 
+private def config : ConfigWithKey :=
+  { transparency := .reducible, iota := false, proj := .no : Config }.toConfigWithKey
+
 mutual
 
 /--
@@ -61,8 +64,8 @@ where
       -- Drawback: cost.
       return e
     else match mode with
-      | .reduce => DiscrTree.reduce e {}
-      | .reduceSimpleOnly => DiscrTree.reduce e { iota := false, proj := .no }
+      | .reduce => DiscrTree.reduce e
+      | .reduceSimpleOnly => withConfigWithKey config <| DiscrTree.reduce e
       | .none => return e
 
   lt (a b : Expr) : MetaM Bool := do

src/Lean/Meta/ArgsPacker.lean

@@ -196,13 +196,13 @@ where
       let packedArg := Unary.pack packedDomain args
       return e.beta #[packedArg]
   | [n] => do
-    withLocalDecl n .default domain fun x => do
+    withLocalDeclD n domain fun x => do
       let dummy := Expr.const ``Unit []
       mkLambdaFVars #[x] (← go packedDomain dummy (args.push x) [])
   | n :: ns =>
     match_expr domain with
     | PSigma a b =>
-      withLocalDecl n .default a fun x => do
+      withLocalDeclD n a fun x => do
         mkLambdaFVars #[x] (← go packedDomain (b.beta #[x]) (args.push x) ns)
     | _ => throwError "curryPSigma: Expected PSigma type, got {domain}"
 
@@ -319,7 +319,7 @@ def uncurryType (types : Array Expr) : MetaM Expr := do
     unless type.isForall do
       throwError "Mutual.uncurryType: Expected forall type, got {type}"
   let domain ← packType (types.map (·.bindingDomain!))
-  withLocalDeclD `x domain fun x => do
+  withLocalDeclD (← mkFreshUserName `x) domain fun x => do
     let codomain ← Mutual.mkCodomain types x
     mkForallFVars #[x] codomain
 
@@ -485,13 +485,14 @@ projects to the `i`th function of type,
 -/
 def curryProj (argsPacker : ArgsPacker) (e : Expr) (i : Nat) : MetaM Expr := do
   let n := argsPacker.numFuncs
-  let packedDomain := (← inferType e).bindingDomain!
+  let t ← inferType e
+  let packedDomain := t.bindingDomain!
   let unaryTypes ← Mutual.unpackType n packedDomain
   unless i < unaryTypes.length do
     throwError "curryProj: index out of range"
   let unaryType := unaryTypes[i]!
   -- unary : (x : a ⊗ b) → e[inl x]
-  let unary ← withLocalDecl `x .default unaryType fun x => do
+  let unary ← withLocalDeclD t.bindingName! unaryType fun x => do
       let packedArg ← Mutual.pack unaryTypes.length packedDomain i x
       mkLambdaFVars #[x] (e.beta #[packedArg])
   -- nary : (x : a) → (y : b) → e[inl (x,y)]

src/Lean/Meta/Basic.lean

@@ -27,6 +27,51 @@ namespace Lean.Meta
 
 builtin_initialize isDefEqStuckExceptionId : InternalExceptionId ← registerInternalExceptionId `isDefEqStuck
 
+def TransparencyMode.toUInt64 : TransparencyMode → UInt64
+  | .all       => 0
+  | .default   => 1
+  | .reducible => 2
+  | .instances => 3
+
+def EtaStructMode.toUInt64 : EtaStructMode → UInt64
+  | .all        => 0
+  | .notClasses => 1
+  | .none       => 2
+
+/--
+Configuration for projection reduction. See `whnfCore`.
+-/
+inductive ProjReductionKind where
+  /-- Projections `s.i` are not reduced at `whnfCore`. -/
+  | no
+  /--
+  Projections `s.i` are reduced at `whnfCore`, and `whnfCore` is used at `s` during the process.
+  Recall that `whnfCore` does not perform `delta` reduction (i.e., it will not unfold constant declarations).
+  -/
+  | yes
+  /--
+  Projections `s.i` are reduced at `whnfCore`, and `whnf` is used at `s` during the process.
+  Recall that `whnfCore` does not perform `delta` reduction (i.e., it will not unfold constant declarations), but `whnf` does.
+  -/
+  | yesWithDelta
+  /--
+  Projections `s.i` are reduced at `whnfCore`, and `whnfAtMostI` is used at `s` during the process.
+  Recall that `whnfAtMostI` is like `whnf` but uses transparency at most `instances`.
+  This option is stronger than `yes`, but weaker than `yesWithDelta`.
+  We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations.
+  When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`,
+  we only want to unify negation (and not all other field operations as well).
+  Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986
+  -/
+  | yesWithDeltaI
+  deriving DecidableEq, Inhabited, Repr
+
+def ProjReductionKind.toUInt64 : ProjReductionKind → UInt64
+  | .no  => 0
+  | .yes => 1
+  | .yesWithDelta => 2
+  | .yesWithDeltaI => 3
+
 /--
 Configuration flags for the `MetaM` monad.
 Many of them are used to control the `isDefEq` function that checks whether two terms are definitionally equal or not.
@@ -118,9 +163,64 @@ structure Config where
   - `max u w =?= mav u ?v` is solved with `?v := w` ignoring the solution `?v := max u w`
   -/
   univApprox : Bool := true
+  /-- If `true`, reduce recursor/matcher applications, e.g., `Nat.rec true (fun _ _ => false) Nat.zero` reduces to `true` -/
+  iota : Bool := true
+  /-- If `true`, reduce terms such as `(fun x => t[x]) a` into `t[a]` -/
+  beta : Bool := true
+  /-- Control projection reduction at `whnfCore`. -/
+  proj : ProjReductionKind := .yesWithDelta
+  /--
+  Zeta reduction: `let x := v; e[x]` reduces to `e[v]`.
+  We say a let-declaration `let x := v; e` is non dependent if it is equivalent to `(fun x => e) v`.
+  Recall that
+  ```
+  fun x : BitVec 5 => let n := 5; fun y : BitVec n => x = y
+  ```
+  is type correct, but
+  ```
+  fun x : BitVec 5 => (fun n => fun y : BitVec n => x = y) 5
+  ```
+  is not.
+  -/
+  zeta : Bool := true
+  /--
+  Zeta-delta reduction: given a local context containing entry `x : t := e`, free variable `x` reduces to `e`.
+  -/
+  zetaDelta : Bool := true
+  deriving Inhabited
+
+/-- Convert `isDefEq` and `WHNF` relevant parts into a key for caching results -/
+private def Config.toKey (c : Config) : UInt64 :=
+  c.transparency.toUInt64 |||
+  (c.foApprox.toUInt64 <<< 2) |||
+  (c.ctxApprox.toUInt64 <<< 3) |||
+  (c.quasiPatternApprox.toUInt64 <<< 4) |||
+  (c.constApprox.toUInt64 <<< 5) |||
+  (c.isDefEqStuckEx.toUInt64 <<< 6) |||
+  (c.unificationHints.toUInt64 <<< 7) |||
+  (c.proofIrrelevance.toUInt64 <<< 8) |||
+  (c.assignSyntheticOpaque.toUInt64 <<< 9) |||
+  (c.offsetCnstrs.toUInt64 <<< 10) |||
+  (c.iota.toUInt64 <<< 11) |||
+  (c.beta.toUInt64 <<< 12) |||
+  (c.zeta.toUInt64 <<< 13) |||
+  (c.zetaDelta.toUInt64 <<< 14) |||
+  (c.univApprox.toUInt64 <<< 15) |||
+  (c.etaStruct.toUInt64 <<< 16) |||
+  (c.proj.toUInt64 <<< 18)
+
+/-- Configuration with key produced by `Config.toKey`. -/
+structure ConfigWithKey where
+  private mk ::
+  config : Config
+  key    : UInt64
+  deriving Inhabited
+
+def Config.toConfigWithKey (c : Config) : ConfigWithKey :=
+  { config := c, key := c.toKey }
 
 /--
-  Function parameter information cache.
+Function parameter information cache.
 -/
 structure ParamInfo where
   /-- The binder annotation for the parameter. -/
@@ -178,7 +278,6 @@ def ParamInfo.isStrictImplicit (p : ParamInfo) : Bool :=
 def ParamInfo.isExplicit (p : ParamInfo) : Bool :=
   p.binderInfo == BinderInfo.default
 
-
 /--
   Function information cache. See `ParamInfo`.
 -/
@@ -192,11 +291,12 @@ structure FunInfo where
   resultDeps : Array Nat       := #[]
 
 /--
-  Key for the function information cache.
+Key for the function information cache.
 -/
 structure InfoCacheKey where
-  /-- The transparency mode used to compute the `FunInfo`. -/
-  transparency : TransparencyMode
+  private mk ::
+  /-- key produced using `Config.toKey`. -/
+  configKey : UInt64
   /-- The function being cached information about. It is quite often an `Expr.const`. -/
   expr         : Expr
   /--
@@ -207,11 +307,10 @@ structure InfoCacheKey where
   nargs?       : Option Nat
   deriving Inhabited, BEq
 
-namespace InfoCacheKey
-instance : Hashable InfoCacheKey :=
-  ⟨fun ⟨transparency, expr, nargs⟩ => mixHash (hash transparency) <| mixHash (hash expr) (hash nargs)⟩
-end InfoCacheKey
+instance : Hashable InfoCacheKey where
+  hash := fun { configKey, expr, nargs? } => mixHash (hash configKey) <| mixHash (hash expr) (hash nargs?)
 
+-- Remark: we don't need to store `Config.toKey` because typeclass resolution uses a fixed configuration.
 structure SynthInstanceCacheKey where
   localInsts        : LocalInstances
   type              : Expr
@@ -231,38 +330,50 @@ structure AbstractMVarsResult where
 
 abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option AbstractMVarsResult)
 
-abbrev InferTypeCache := PersistentExprStructMap Expr
+-- Key for `InferType` and `WHNF` caches
+structure ExprConfigCacheKey where
+  private mk ::
+  expr      : Expr
+  configKey : UInt64
+  deriving Inhabited
+
+instance : BEq ExprConfigCacheKey where
+  beq a b :=
+    Expr.equal a.expr b.expr &&
+    a.configKey == b.configKey
+
+instance : Hashable ExprConfigCacheKey where
+  hash := fun { expr, configKey } => mixHash (hash expr) (hash configKey)
+
+abbrev InferTypeCache := PersistentHashMap ExprConfigCacheKey Expr
 abbrev FunInfoCache   := PersistentHashMap InfoCacheKey FunInfo
-abbrev WhnfCache      := PersistentExprStructMap Expr
+abbrev WhnfCache      := PersistentHashMap ExprConfigCacheKey Expr
+
+structure DefEqCacheKey where
+  private mk ::
+  lhs       : Expr
+  rhs       : Expr
+  configKey : UInt64
+  deriving Inhabited, BEq
+
+instance : Hashable DefEqCacheKey where
+  hash := fun { lhs, rhs, configKey } => mixHash (hash lhs) <| mixHash (hash rhs) (hash configKey)
 
 /--
-  A mapping `(s, t) ↦ isDefEq s t` per transparency level.
-  TODO: consider more efficient representations (e.g., a proper set) and caching policies (e.g., imperfect cache).
-  We should also investigate the impact on memory consumption. -/
-structure DefEqCache where
-  reducible : PersistentHashMap (Expr × Expr) Bool := {}
-  instances : PersistentHashMap (Expr × Expr) Bool := {}
-  default   : PersistentHashMap (Expr × Expr) Bool := {}
-  all       : PersistentHashMap (Expr × Expr) Bool := {}
-  deriving Inhabited
-
-/--
-  A cache for `inferType` at transparency levels `.default` an `.all`.
+A mapping `(s, t) ↦ isDefEq s t`.
+TODO: consider more efficient representations (e.g., a proper set) and caching policies (e.g., imperfect cache).
+We should also investigate the impact on memory consumption.
 -/
-structure InferTypeCaches where
-  default   : InferTypeCache
-  all       : InferTypeCache
-  deriving Inhabited
+abbrev DefEqCache := PersistentHashMap DefEqCacheKey Bool
 
 /--
-  Cache datastructures for type inference, type class resolution, whnf, and definitional equality.
+Cache datastructures for type inference, type class resolution, whnf, and definitional equality.
 -/
 structure Cache where
-  inferType      : InferTypeCaches := ⟨{}, {}⟩
+  inferType      : InferTypeCache := {}
   funInfo        : FunInfoCache := {}
   synthInstance  : SynthInstanceCache := {}
-  whnfDefault    : WhnfCache := {} -- cache for closed terms and `TransparencyMode.default`
-  whnfAll        : WhnfCache := {} -- cache for closed terms and `TransparencyMode.all`
+  whnf           : WhnfCache := {}
   defEqTrans     : DefEqCache := {} -- transient cache for terms containing mvars or using nonstandard configuration options, it is frequently reset.
   defEqPerm      : DefEqCache := {} -- permanent cache for terms not containing mvars and using standard configuration options
   deriving Inhabited
@@ -333,6 +444,7 @@ register_builtin_option maxSynthPendingDepth : Nat := {
 -/
 structure Context where
   private config    : Config               := {}
+  private configKey : UInt64               := config.toKey
   /-- Local context -/
   lctx              : LocalContext         := {}
   /-- Local instances in `lctx`. -/
@@ -483,17 +595,27 @@ variable [MonadControlT MetaM n] [Monad n]
 @[inline] def modifyCache (f : Cache → Cache) : MetaM Unit :=
   modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed, diag }
 
-@[inline] def modifyInferTypeCacheDefault (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
-  modifyCache fun ⟨⟨icd, ica⟩, c1, c2, c3, c4, c5, c6⟩ => ⟨⟨f icd, ica⟩, c1, c2, c3, c4, c5, c6⟩
-
-@[inline] def modifyInferTypeCacheAll (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
-  modifyCache fun ⟨⟨icd, ica⟩, c1, c2, c3, c4, c5, c6⟩ => ⟨⟨icd, f ica⟩, c1, c2, c3, c4, c5, c6⟩
+@[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
+  modifyCache fun ⟨ic, c1, c2, c3, c4, c5⟩ => ⟨f ic, c1, c2, c3, c4, c5⟩
 
 @[inline] def modifyDefEqTransientCache (f : DefEqCache → DefEqCache) : MetaM Unit :=
-  modifyCache fun ⟨c1, c2, c3, c4, c5, defeqTrans, c6⟩ => ⟨c1, c2, c3, c4, c5, f defeqTrans, c6⟩
+  modifyCache fun ⟨c1, c2, c3, c4, defeqTrans, c5⟩ => ⟨c1, c2, c3, c4, f defeqTrans, c5⟩
 
 @[inline] def modifyDefEqPermCache (f : DefEqCache → DefEqCache) : MetaM Unit :=
-  modifyCache fun ⟨c1, c2, c3, c4, c5, c6, defeqPerm⟩ => ⟨c1, c2, c3, c4, c5, c6, f defeqPerm⟩
+  modifyCache fun ⟨c1, c2, c3, c4, c5, defeqPerm⟩ => ⟨c1, c2, c3, c4, c5, f defeqPerm⟩
+
+def mkExprConfigCacheKey (expr : Expr) : MetaM ExprConfigCacheKey :=
+  return { expr, configKey := (← read).configKey }
+
+def mkDefEqCacheKey (lhs rhs : Expr) : MetaM DefEqCacheKey := do
+  let configKey := (← read).configKey
+  if Expr.quickLt lhs rhs then
+    return { lhs, rhs, configKey }
+  else
+    return { lhs := rhs, rhs := lhs, configKey }
+
+def mkInfoCacheKey (expr : Expr) (nargs? : Option Nat) : MetaM InfoCacheKey :=
+  return { expr, nargs?, configKey := (← read).configKey }
 
 @[inline] def resetDefEqPermCaches : MetaM Unit :=
   modifyDefEqPermCache fun _ => {}
@@ -538,6 +660,9 @@ def getLocalInstances : MetaM LocalInstances :=
 def getConfig : MetaM Config :=
   return (← read).config
 
+def getConfigWithKey : MetaM ConfigWithKey :=
+  return (← getConfig).toConfigWithKey
+
 def resetZetaDeltaFVarIds : MetaM Unit :=
   modify fun s => { s with zetaDeltaFVarIds := {} }
 
@@ -941,7 +1066,16 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) :
 
 /-- `withConfig f x` executes `x` using the updated configuration object obtained by applying `f`. -/
 @[inline] def withConfig (f : Config → Config) : n α → n α :=
-  mapMetaM <| withReader (fun ctx => { ctx with config := f ctx.config })
+  mapMetaM <| withReader fun ctx =>
+    let config := f ctx.config
+    let configKey := config.toKey
+    { ctx with config, configKey }
+
+@[inline] def withConfigWithKey (c : ConfigWithKey) : n α → n α :=
+  mapMetaM <| withReader fun ctx =>
+    let config := c.config
+    let configKey := c.key
+    { ctx with config, configKey }
 
 @[inline] def withCanUnfoldPred (p : Config → ConstantInfo → CoreM Bool) : n α → n α :=
   mapMetaM <| withReader (fun ctx => { ctx with canUnfold? := p })
@@ -961,8 +1095,15 @@ Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true`
 @[inline] def withoutProofIrrelevance (x : n α) : n α :=
   withConfig (fun cfg => { cfg with proofIrrelevance := false }) x
 
+@[inline] private def Context.setTransparency (ctx : Context) (transparency : TransparencyMode) : Context :=
+  let config := { ctx.config with transparency }
+  -- Recall that `transparency` is stored in the first 2 bits
+  let configKey : UInt64 := ((ctx.configKey >>> (2 : UInt64)) <<< 2) ||| transparency.toUInt64
+  { ctx with config, configKey }
+
 @[inline] def withTransparency (mode : TransparencyMode) : n α → n α :=
-  withConfig (fun config => { config with transparency := mode })
+  -- We avoid `withConfig` for performance reasons.
+  mapMetaM <| withReader (·.setTransparency mode)
 
 /-- `withDefault x` executes `x` using the default transparency setting. -/
 @[inline] def withDefault (x : n α) : n α :=
@@ -983,13 +1124,10 @@ or type class instances are unfolded.
 Execute `x` ensuring the transparency setting is at least `mode`.
 Recall that `.all > .default > .instances > .reducible`.
 -/
-@[inline] def withAtLeastTransparency (mode : TransparencyMode) (x : n α) : n α :=
-  withConfig
-    (fun config =>
-      let oldMode := config.transparency
-      let mode    := if oldMode.lt mode then mode else oldMode
-      { config with transparency := mode })
-    x
+@[inline] def withAtLeastTransparency (mode : TransparencyMode) : n α → n α :=
+  mapMetaM <| withReader fun ctx =>
+    let modeOld := ctx.config.transparency
+    ctx.setTransparency <| if modeOld.lt mode then mode else modeOld
 
 /-- Execute `x` allowing `isDefEq` to assign synthetic opaque metavariables. -/
 @[inline] def withAssignableSyntheticOpaque (x : n α) : n α :=
@@ -1011,8 +1149,8 @@ def getTheoremInfo (info : ConstantInfo) : MetaM (Option ConstantInfo) := do
 
 private def getDefInfoTemp (info : ConstantInfo) : MetaM (Option ConstantInfo) := do
   match (← getTransparency) with
-  | TransparencyMode.all => return some info
-  | TransparencyMode.default => return some info
+  | .all => return some info
+  | .default => return some info
   | _ =>
     if (← isReducible info.name) then
       return some info

src/Lean/Meta/Canonicalizer.lean

@@ -91,7 +91,15 @@ private partial def mkKey (e : Expr) : CanonM UInt64 := do
           let eNew ← instantiateMVars e
           unless eNew == e do
             return (← mkKey eNew)
-        let info ← getFunInfo f
+        let info ← if f.hasLooseBVars then
+          -- If `f` has loose bound variables, `getFunInfo` will fail.
+          -- This can only happen if `f` contains local variables.
+          -- Instead we use an empty `FunInfo`, which results in the
+          -- `i < info.paramInfo.size` check below failing for all indices,
+          -- and hence mixing in the hash for all arguments.
+          pure {}
+        else
+          getFunInfo f
         let mut k ← mkKey f
         for i in [:e.getAppNumArgs] do
           if h : i < info.paramInfo.size then
@@ -101,10 +109,13 @@ private partial def mkKey (e : Expr) : CanonM UInt64 := do
           else
               k := mixHash k (← mkKey (e.getArg! i))
         return k
-      | .lam _ t b _
-      | .forallE _ t b _ =>
+      | .lam n t b bi
+      | .forallE n t b bi =>
+        -- Note that we do not use `withLocalDecl` here, for performance reasons.
+        -- Instead we have a guard for loose bound variables in the `.app` case above.
         return mixHash (← mkKey t) (← mkKey b)
-      | .letE _ _ v b _ =>
+      | .letE n t v b _ =>
+        -- Similarly, we do not use `withLetDecl` here.
         return mixHash (← mkKey v) (← mkKey b)
       | .proj _ i s =>
         return mixHash i.toUInt64 (← mkKey s)
@@ -124,11 +135,11 @@ def canon (e : Expr) : CanonM Expr := do
         if (← isDefEq e e') then
           return e'
       -- `e` is not definitionally equal to any expression in `es'`. We claim this should be rare.
-      unsafe modify fun { cache, keyToExprs } => { cache, keyToExprs := keyToExprs.insert k (e :: es') }
+      modify fun { cache, keyToExprs } => { cache, keyToExprs := keyToExprs.insert k (e :: es') }
       return e
   else
     -- `e` is the first expression we found with key `k`.
-    unsafe modify fun { cache, keyToExprs } => { cache, keyToExprs := keyToExprs.insert k [e] }
+    modify fun { cache, keyToExprs } => { cache, keyToExprs := keyToExprs.insert k [e] }
     return e
 
 end Canonicalizer

src/Lean/Meta/DiscrTree.lean

@@ -305,16 +305,13 @@ def hasNoindexAnnotation (e : Expr) : Bool :=
 
 /--
 Reduction procedure for the discrimination tree indexing.
-The parameter `config` controls how aggressively the term is reduced.
-The parameter at type `DiscrTree` controls this value.
-See comment at `DiscrTree`.
 -/
-partial def reduce (e : Expr) (config : WhnfCoreConfig) : MetaM Expr := do
-  let e ← whnfCore e config
+partial def reduce (e : Expr) : MetaM Expr := do
+  let e ← whnfCore e
   match (← unfoldDefinition? e) with
-  | some e => reduce e config
+  | some e => reduce e
   | none => match e.etaExpandedStrict? with
-    | some e => reduce e config
+    | some e => reduce e
     | none   => return e
 
 /--
@@ -333,24 +330,24 @@ private def isBadKey (fn : Expr) : Bool :=
   | _           => true
 
 /--
-  Reduce `e` until we get an irreducible term (modulo current reducibility setting) or the resulting term
-  is a bad key (see comment at `isBadKey`).
-  We use this method instead of `reduce` for root terms at `pushArgs`. -/
-private partial def reduceUntilBadKey (e : Expr) (config : WhnfCoreConfig) : MetaM Expr := do
+Reduce `e` until we get an irreducible term (modulo current reducibility setting) or the resulting term
+is a bad key (see comment at `isBadKey`).
+We use this method instead of `reduce` for root terms at `pushArgs`. -/
+private partial def reduceUntilBadKey (e : Expr) : MetaM Expr := do
   let e ← step e
   match e.etaExpandedStrict? with
-  | some e => reduceUntilBadKey e config
+  | some e => reduceUntilBadKey e
   | none   => return e
 where
   step (e : Expr) := do
-    let e ← whnfCore e config
+    let e ← whnfCore e
     match (← unfoldDefinition? e) with
     | some e' => if isBadKey e'.getAppFn then return e else step e'
     | none    => return e
 
 /-- whnf for the discrimination tree module -/
-def reduceDT (e : Expr) (root : Bool) (config : WhnfCoreConfig) : MetaM Expr :=
-  if root then reduceUntilBadKey e config else reduce e config
+def reduceDT (e : Expr) (root : Bool) : MetaM Expr :=
+  if root then reduceUntilBadKey e else reduce e
 
 /- Remark: we use `shouldAddAsStar` only for nested terms, and `root == false` for nested terms -/
 
@@ -372,11 +369,11 @@ In this issue, we have a local hypotheses `(h : ∀ p : α × β, f p p.2 = p.2)
 For example, it was introduced by another tactic. Thus, when populating the discrimination tree explicit arguments provided to `simp` (e.g., `simp [h]`),
 we use `noIndexAtArgs := true`. See comment: https://github.com/leanprover/lean4/issues/2670#issuecomment-1758889365
 -/
-private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : WhnfCoreConfig) (noIndexAtArgs : Bool) : MetaM (Key × Array Expr) := do
+private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (noIndexAtArgs : Bool) : MetaM (Key × Array Expr) := do
   if hasNoindexAnnotation e then
     return (.star, todo)
   else
-    let e ← reduceDT e root config
+    let e ← reduceDT e root
     let fn := e.getAppFn
     let push (k : Key) (nargs : Nat) (todo : Array Expr): MetaM (Key × Array Expr) := do
       let info ← getFunInfoNArgs fn nargs
@@ -422,23 +419,23 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : Whnf
     | _ => return (.other, todo)
 
 @[inherit_doc pushArgs]
-partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) (config : WhnfCoreConfig) (noIndexAtArgs : Bool) : MetaM (Array Key) := do
+partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) (noIndexAtArgs : Bool) : MetaM (Array Key) := do
   if todo.isEmpty then
     return keys
   else
     let e    := todo.back!
     let todo := todo.pop
-    let (k, todo) ← pushArgs root todo e config noIndexAtArgs
-    mkPathAux false todo (keys.push k) config noIndexAtArgs
+    let (k, todo) ← pushArgs root todo e noIndexAtArgs
+    mkPathAux false todo (keys.push k) noIndexAtArgs
 
 private def initCapacity := 8
 
 @[inherit_doc pushArgs]
-def mkPath (e : Expr) (config : WhnfCoreConfig) (noIndexAtArgs := false) : MetaM (Array Key) := do
+def mkPath (e : Expr) (noIndexAtArgs := false) : MetaM (Array Key) := do
   withReducible do
     let todo : Array Expr := .mkEmpty initCapacity
     let keys : Array Key := .mkEmpty initCapacity
-    mkPathAux (root := true) (todo.push e) keys config noIndexAtArgs
+    mkPathAux (root := true) (todo.push e) keys noIndexAtArgs
 
 private partial def createNodes (keys : Array Key) (v : α) (i : Nat) : Trie α :=
   if h : i < keys.size then
@@ -492,23 +489,23 @@ def insertCore [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTr
       let c := insertAux keys v 1 c
       { root := d.root.insert k c }
 
-def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : WhnfCoreConfig) (noIndexAtArgs := false) : MetaM (DiscrTree α) := do
-  let keys ← mkPath e config noIndexAtArgs
+def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (noIndexAtArgs := false) : MetaM (DiscrTree α) := do
+  let keys ← mkPath e noIndexAtArgs
   return d.insertCore keys v
 
 /--
 Inserts a value into a discrimination tree,
 but only if its key is not of the form `#[*]` or `#[=, *, *, *]`.
 -/
-def insertIfSpecific [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : WhnfCoreConfig) (noIndexAtArgs := false) : MetaM (DiscrTree α) := do
-  let keys ← mkPath e config noIndexAtArgs
+def insertIfSpecific [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (noIndexAtArgs := false) : MetaM (DiscrTree α) := do
+  let keys ← mkPath e noIndexAtArgs
   return if keys == #[Key.star] || keys == #[Key.const `Eq 3, Key.star, Key.star, Key.star] then
     d
   else
     d.insertCore keys v
 
-private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) := do
-  let e ← reduceDT e root config
+private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Expr) := do
+  let e ← reduceDT e root
   unless root do
     -- See pushArgs
     if let some v := toNatLit? e then
@@ -580,11 +577,11 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig
   | .forallE _ d _ _ => return (.arrow, #[d])
   | _ => return (.other, #[])
 
-private abbrev getMatchKeyArgs (e : Expr) (root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) :=
-  getKeyArgs e (isMatch := true) (root := root) (config := config)
+private abbrev getMatchKeyArgs (e : Expr) (root : Bool) : MetaM (Key × Array Expr) :=
+  getKeyArgs e (isMatch := true) (root := root)
 
-private abbrev getUnifyKeyArgs (e : Expr) (root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) :=
-  getKeyArgs e (isMatch := false) (root := root) (config := config)
+private abbrev getUnifyKeyArgs (e : Expr) (root : Bool) : MetaM (Key × Array Expr) :=
+  getKeyArgs e (isMatch := false) (root := root)
 
 private def getStarResult (d : DiscrTree α) : Array α :=
   let result : Array α := .mkEmpty initCapacity
@@ -595,7 +592,7 @@ private def getStarResult (d : DiscrTree α) : Array α :=
 private abbrev findKey (cs : Array (Key × Trie α)) (k : Key) : Option (Key × Trie α) :=
   cs.binSearch (k, default) (fun a b => a.1 < b.1)
 
-private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Array α) (config : WhnfCoreConfig) : MetaM (Array α) := do
+private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Array α) : MetaM (Array α) := do
   match c with
   | .node vs cs =>
     if todo.isEmpty then
@@ -606,48 +603,48 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
       let e     := todo.back!
       let todo  := todo.pop
       let first := cs[0]! /- Recall that `Key.star` is the minimal key -/
-      let (k, args) ← getMatchKeyArgs e (root := false) config
+      let (k, args) ← getMatchKeyArgs e (root := false)
       /- We must always visit `Key.star` edges since they are wildcards.
          Thus, `todo` is not used linearly when there is `Key.star` edge
          and there is an edge for `k` and `k != Key.star`. -/
       let visitStar (result : Array α) : MetaM (Array α) :=
         if first.1 == .star then
-          getMatchLoop todo first.2 result config
+          getMatchLoop todo first.2 result
         else
           return result
       let visitNonStar (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
         match findKey cs k with
         | none   => return result
-        | some c => getMatchLoop (todo ++ args) c.2 result config
+        | some c => getMatchLoop (todo ++ args) c.2 result
       let result ← visitStar result
       match k with
       | .star  => return result
       | _      => visitNonStar k args result
 
-private def getMatchRoot (d : DiscrTree α) (k : Key) (args : Array Expr) (result : Array α) (config : WhnfCoreConfig) : MetaM (Array α) :=
+private def getMatchRoot (d : DiscrTree α) (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
   match d.root.find? k with
   | none   => return result
-  | some c => getMatchLoop args c result config
+  | some c => getMatchLoop args c result
 
-private def getMatchCore (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) : MetaM (Key × Array α) :=
+private def getMatchCore (d : DiscrTree α) (e : Expr) : MetaM (Key × Array α) :=
   withReducible do
     let result := getStarResult d
-    let (k, args) ← getMatchKeyArgs e (root := true) config
+    let (k, args) ← getMatchKeyArgs e (root := true)
     match k with
     | .star  => return (k, result)
-    | _      => return (k, (← getMatchRoot d k args result config))
+    | _      => return (k, (← getMatchRoot d k args result))
 
 /--
   Find values that match `e` in `d`.
 -/
-def getMatch (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) : MetaM (Array α) :=
-  return (← getMatchCore d e config).2
+def getMatch (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
+  return (← getMatchCore d e).2
 
 /--
   Similar to `getMatch`, but returns solutions that are prefixes of `e`.
   We store the number of ignored arguments in the result.-/
-partial def getMatchWithExtra (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) : MetaM (Array (α × Nat)) := do
-  let (k, result) ← getMatchCore d e config
+partial def getMatchWithExtra (d : DiscrTree α) (e : Expr) : MetaM (Array (α × Nat)) := do
+  let (k, result) ← getMatchCore d e
   let result := result.map (·, 0)
   if !e.isApp then
     return result
@@ -669,7 +666,7 @@ where
     | _               => return false
 
   go (e : Expr) (numExtra : Nat) (result : Array (α × Nat)) : MetaM (Array (α × Nat)) := do
-    let result := result ++ (← getMatchCore d e config).2.map (., numExtra)
+    let result := result ++ (← getMatchCore d e).2.map (., numExtra)
     if e.isApp then
       go e.appFn! (numExtra + 1) result
     else
@@ -678,8 +675,8 @@ where
 /--
 Return the root symbol for `e`, and the number of arguments after `reduceDT`.
 -/
-def getMatchKeyRootFor (e : Expr) (config : WhnfCoreConfig) : MetaM (Key × Nat) := do
-  let e ← reduceDT e (root := true) config
+def getMatchKeyRootFor (e : Expr) : MetaM (Key × Nat) := do
+  let e ← reduceDT e (root := true)
   let numArgs := e.getAppNumArgs
   let key := match e.getAppFn with
     | .lit v         => .lit v
@@ -716,17 +713,17 @@ We use this method to simulate Lean 3's indexing.
 
 The natural number in the result is the number of arguments in `e` after `reduceDT`.
 -/
-def getMatchLiberal (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) : MetaM (Array α × Nat) := do
+def getMatchLiberal (d : DiscrTree α) (e : Expr) : MetaM (Array α × Nat) := do
   withReducible do
     let result := getStarResult d
-    let (k, numArgs) ← getMatchKeyRootFor e config
+    let (k, numArgs) ← getMatchKeyRootFor e
     match k with
     | .star  => return (result, numArgs)
     | _      => return (getAllValuesForKey d k result, numArgs)
 
-partial def getUnify (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) : MetaM (Array α) :=
+partial def getUnify (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
   withReducible do
-    let (k, args) ← getUnifyKeyArgs e (root := true) config
+    let (k, args) ← getUnifyKeyArgs e (root := true)
     match k with
     | .star => d.root.foldlM (init := #[]) fun result k c => process k.arity #[] c result
     | _ =>
@@ -750,7 +747,7 @@ where
       else
         let e     := todo.back!
         let todo  := todo.pop
-        let (k, args) ← getUnifyKeyArgs e (root := false) config
+        let (k, args) ← getUnifyKeyArgs e (root := false)
         let visitStar (result : Array α) : MetaM (Array α) :=
           let first := cs[0]!
           if first.1 == .star then

src/Lean/Meta/ExprDefEq.lean

@@ -2079,50 +2079,37 @@ Structure for storing defeq cache key information.
 -/
 structure DefEqCacheKeyInfo where
   kind : DefEqCacheKind
-  key  : Expr × Expr
+  key  : DefEqCacheKey
 
 private def mkCacheKey (t s : Expr) : MetaM DefEqCacheKeyInfo := do
   let kind ← getDefEqCacheKind t s
-  let key := if Expr.quickLt t s then (t, s) else (s, t)
+  let key ← mkDefEqCacheKey t s
   return { key, kind }
 
 private def getCachedResult (keyInfo : DefEqCacheKeyInfo) : MetaM LBool := do
   let cache ← match keyInfo.kind with
     | .transient => pure (← get).cache.defEqTrans
     | .permanent => pure (← get).cache.defEqPerm
-  let cache := match (← getTransparency) with
-    | .reducible => cache.reducible
-    | .instances => cache.instances
-    | .default   => cache.default
-    | .all       => cache.all
   match cache.find? keyInfo.key with
   | some val => return val.toLBool
   | none => return .undef
 
-def DefEqCache.update (cache : DefEqCache) (mode : TransparencyMode) (key : Expr × Expr) (result : Bool) : DefEqCache :=
-  match mode with
-  | .reducible => { cache with reducible := cache.reducible.insert key result }
-  | .instances => { cache with instances := cache.instances.insert key result }
-  | .default   => { cache with default   := cache.default.insert key result }
-  | .all       => { cache with all       := cache.all.insert key result }
-
 private def cacheResult (keyInfo : DefEqCacheKeyInfo) (result : Bool) : MetaM Unit := do
-  let mode ← getTransparency
   let key := keyInfo.key
   match keyInfo.kind with
-  | .permanent => modifyDefEqPermCache fun c => c.update mode key result
+  | .permanent => modifyDefEqPermCache fun c => c.insert key result
   | .transient =>
     /-
     We must ensure that all assigned metavariables in the key are replaced by their current assignments.
     Otherwise, the key is invalid after the assignment is "backtracked".
     See issue #1870 for an example.
     -/
-    let key := (← instantiateMVars key.1, ← instantiateMVars key.2)
-    modifyDefEqTransientCache fun c => c.update mode key result
+    let key ← mkDefEqCacheKey (← instantiateMVars key.lhs) (← instantiateMVars key.rhs)
+    modifyDefEqTransientCache fun c => c.insert key result
 
 private def whnfCoreAtDefEq (e : Expr) : MetaM Expr := do
   if backward.isDefEq.lazyWhnfCore.get (← getOptions) then
-    whnfCore e (config := { proj := .yesWithDeltaI })
+    withConfig (fun ctx => { ctx with proj := .yesWithDeltaI }) <| whnfCore e
   else
     whnfCore e
 

src/Lean/Meta/FunInfo.lean

@@ -10,13 +10,13 @@ import Lean.Meta.InferType
 namespace Lean.Meta
 
 @[inline] private def checkFunInfoCache (fn : Expr) (maxArgs? : Option Nat) (k : MetaM FunInfo) : MetaM FunInfo := do
-  let t ← getTransparency
-  match (← get).cache.funInfo.find? ⟨t, fn, maxArgs?⟩ with
-  | some finfo => pure finfo
+  let key ← mkInfoCacheKey fn maxArgs?
+  match (← get).cache.funInfo.find? key with
+  | some finfo => return finfo
   | none       => do
     let finfo ← k
-    modify fun s => { s with cache := { s.cache with funInfo := s.cache.funInfo.insert ⟨t, fn, maxArgs?⟩ finfo } }
-    pure finfo
+    modify fun s => { s with cache := { s.cache with funInfo := s.cache.funInfo.insert key finfo } }
+    return finfo
 
 @[inline] private def whenHasVar {α} (e : Expr) (deps : α) (k : α → α) : α :=
   if e.hasFVar then k deps else deps

src/Lean/Meta/InferType.lean

@@ -97,8 +97,8 @@ private def inferConstType (c : Name) (us : List Level) : MetaM Expr := do
 private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Expr := do
   let structType ← inferType e
   let structType ← whnf structType
-  let failed {α} : Unit → MetaM α := fun _ =>
-    throwError "invalid projection{indentExpr (mkProj structName idx e)} from type {structType}"
+  let failed {α} : Unit → MetaM α := fun _ => do
+    throwError "invalid projection{indentExpr (mkProj structName idx e)}\nfrom type{indentExpr structType}"
   matchConstStructure structType.getAppFn failed fun structVal structLvls ctorVal =>
     let structTypeArgs := structType.getAppArgs
     if structVal.numParams + structVal.numIndices != structTypeArgs.size then
@@ -165,24 +165,27 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do
   | none   => fvarId.throwUnknown
 
 @[inline] private def checkInferTypeCache (e : Expr) (inferType : MetaM Expr) : MetaM Expr := do
-  match (← getTransparency) with
-  | .default =>
-    match (← get).cache.inferType.default.find? e with
+  if e.hasMVar then
+    inferType
+  else
+    let key ← mkExprConfigCacheKey e
+    match (← get).cache.inferType.find? key with
     | some type => return type
     | none =>
       let type ← inferType
-      unless e.hasMVar || type.hasMVar do
-        modifyInferTypeCacheDefault fun c => c.insert e type
+      unless type.hasMVar do
+        modifyInferTypeCache fun c => c.insert key type
       return type
-  | .all =>
-    match (← get).cache.inferType.all.find? e with
-    | some type => return type
-    | none =>
-      let type ← inferType
-      unless e.hasMVar || type.hasMVar do
-        modifyInferTypeCacheAll fun c => c.insert e type
-      return type
-  | _ => panic! "checkInferTypeCache: transparency mode not default or all"
+
+private def defaultConfig : ConfigWithKey :=
+  { : Config }.toConfigWithKey
+
+private def allConfig : ConfigWithKey :=
+  { transparency := .all : Config }.toConfigWithKey
+
+@[inline] def withInferTypeConfig (x : MetaM α) : MetaM α := do
+  let cfg := if (← getTransparency) == .all then allConfig else defaultConfig
+  withConfigWithKey cfg x
 
 @[export lean_infer_type]
 def inferTypeImp (e : Expr) : MetaM Expr :=
@@ -201,7 +204,7 @@ def inferTypeImp (e : Expr) : MetaM Expr :=
     | .forallE ..    => checkInferTypeCache e (inferForallType e)
     | .lam ..        => checkInferTypeCache e (inferLambdaType e)
     | .letE ..       => checkInferTypeCache e (inferLambdaType e)
-  withIncRecDepth <| withAtLeastTransparency TransparencyMode.default (infer e)
+  withIncRecDepth <| withInferTypeConfig (infer e)
 
 /--
   Return `LBool.true` if given level is always equivalent to universe level zero.

src/Lean/Meta/Instances.lean

@@ -72,9 +72,6 @@ structure Instances where
   erased        : PHashSet Name := {}
   deriving Inhabited
 
-/-- Configuration for the discrimination tree module -/
-def tcDtConfig : WhnfCoreConfig := {}
-
 def addInstanceEntry (d : Instances) (e : InstanceEntry) : Instances :=
   match e.globalName? with
   | some n => { d with discrTree := d.discrTree.insertCore e.keys e, instanceNames := d.instanceNames.insert n e, erased := d.erased.erase n }
@@ -98,7 +95,7 @@ private def mkInstanceKey (e : Expr) : MetaM (Array InstanceKey) := do
   let type ← inferType e
   withNewMCtxDepth do
     let (_, _, type) ← forallMetaTelescopeReducing type
-    DiscrTree.mkPath type tcDtConfig
+    DiscrTree.mkPath type
 
 /--
 Compute the order the arguments of `inst` should be synthesized.

src/Lean/Meta/LazyDiscrTree.lean

@@ -184,9 +184,9 @@ private def elimLooseBVarsByBeta (e : Expr) : CoreM Expr :=
       else
         return .continue)
 
-private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig) :
+private def getKeyArgs (e : Expr) (isMatch root : Bool) :
     MetaM (Key × Array Expr) := do
-  let e ← DiscrTree.reduceDT e root config
+  let e ← DiscrTree.reduceDT e root
   unless root do
     -- See pushArgs
     if let some v := toNatLit? e then
@@ -259,9 +259,9 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig
 /-
 Given an expression we are looking for patterns that match, return the key and sub-expressions.
 -/
-private abbrev getMatchKeyArgs (e : Expr) (root : Bool) (config : WhnfCoreConfig) :
+private abbrev getMatchKeyArgs (e : Expr) (root : Bool) :
     MetaM (Key × Array Expr) :=
-  getKeyArgs e (isMatch := true) (root := root) (config := config)
+  getKeyArgs e (isMatch := true) (root := root)
 
 end MatchClone
 
@@ -313,8 +313,6 @@ discriminator key is computed and processing the remaining
 terms is deferred until demanded by a match.
 -/
 structure LazyDiscrTree (α : Type) where
-  /-- Configuration for normalization. -/
-  config : Lean.Meta.WhnfCoreConfig := {}
   /-- Backing array of trie entries.  Should be owned by this trie. -/
   tries : Array (LazyDiscrTree.Trie α) := #[default]
   /-- Map from discriminator trie roots to the index. -/
@@ -332,12 +330,12 @@ open Lean.Meta.DiscrTree (mkNoindexAnnotation hasNoindexAnnotation reduceDT)
 /--
 Specialization of Lean.Meta.DiscrTree.pushArgs
 -/
-private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : WhnfCoreConfig) :
+private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) :
     MetaM (Key × Array Expr) := do
   if hasNoindexAnnotation e then
     return (.star, todo)
   else
-    let e ← reduceDT e root config
+    let e ← reduceDT e root
     let fn := e.getAppFn
     let push (k : Key) (nargs : Nat) (todo : Array Expr) : MetaM (Key × Array Expr) := do
       let info ← getFunInfoNArgs fn nargs
@@ -389,8 +387,8 @@ private def initCapacity := 8
 /--
 Get the root key and rest of terms of an expression using the specified config.
 -/
-private def rootKey (cfg: WhnfCoreConfig) (e : Expr) : MetaM (Key × Array Expr) :=
-  pushArgs true (Array.mkEmpty initCapacity) e cfg
+private def rootKey (e : Expr) : MetaM (Key × Array Expr) :=
+  pushArgs true (Array.mkEmpty initCapacity) e
 
 private partial def buildPath (op : Bool → Array Expr → Expr → MetaM (Key × Array Expr)) (root : Bool) (todo : Array Expr) (keys : Array Key) : MetaM (Array Key) := do
   if todo.isEmpty then
@@ -407,9 +405,9 @@ Create a key path from an expression using the function used for patterns.
 This differs from Lean.Meta.DiscrTree.mkPath and targetPath in that the expression
 should uses free variables rather than meta-variables for holes.
 -/
-def patternPath (e : Expr) (config : WhnfCoreConfig) : MetaM (Array Key) := do
+def patternPath (e : Expr) : MetaM (Array Key) := do
   let todo : Array Expr := .mkEmpty initCapacity
-  let op root todo e := pushArgs root todo e config
+  let op root todo e := pushArgs root todo e
   buildPath op (root := true) (todo.push e) (.mkEmpty initCapacity)
 
 /--
@@ -417,21 +415,21 @@ Create a key path from an expression we are matching against.
 
 This should have mvars instantiated where feasible.
 -/
-def targetPath (e : Expr) (config : WhnfCoreConfig) : MetaM (Array Key) := do
+def targetPath (e : Expr) : MetaM (Array Key) := do
   let todo : Array Expr := .mkEmpty initCapacity
   let op root todo e := do
-        let (k, args) ← MatchClone.getMatchKeyArgs e root config
+        let (k, args) ← MatchClone.getMatchKeyArgs e root
         pure (k, todo ++ args)
   buildPath op (root := true) (todo.push e) (.mkEmpty initCapacity)
 
 /- Monad for finding matches while resolving deferred patterns. -/
 @[reducible]
-private def MatchM α := ReaderT WhnfCoreConfig (StateRefT (Array (Trie α)) MetaM)
+private def MatchM α := StateRefT (Array (Trie α)) MetaM
 
 private def runMatch (d : LazyDiscrTree α) (m : MatchM α β)  : MetaM (β × LazyDiscrTree α) := do
-  let { config := c, tries := a, roots := r } := d
-  let (result, a) ← withReducible $ (m.run c).run a
-  pure (result, { config := c, tries := a, roots := r})
+  let { tries := a, roots := r } := d
+  let (result, a) ← withReducible <| m.run a
+  return (result, { tries := a, roots := r})
 
 private def setTrie (i : TrieIndex) (v : Trie α) : MatchM α Unit :=
   modify (·.set! i v)
@@ -444,7 +442,7 @@ private def newTrie [Monad m] [MonadState (Array (Trie α)) m] (e : LazyEntry α
 private def addLazyEntryToTrie (i:TrieIndex) (e : LazyEntry α) : MatchM α Unit :=
   modify (·.modify i (·.pushPending e))
 
-private def evalLazyEntry (config : WhnfCoreConfig)
+private def evalLazyEntry
     (p : Array α × TrieIndex × Std.HashMap Key TrieIndex)
     (entry : LazyEntry α)
     : MatchM α (Array α × TrieIndex × Std.HashMap Key TrieIndex) := do
@@ -456,7 +454,7 @@ private def evalLazyEntry (config : WhnfCoreConfig)
   else
     let e    := todo.back!
     let todo := todo.pop
-    let (k, todo) ← withLCtx lctx.1 lctx.2 $ pushArgs false todo e config
+    let (k, todo) ← withLCtx lctx.1 lctx.2 <| pushArgs false todo e
     if k == .star then
       if starIdx = 0 then
         let starIdx ← newTrie (todo, lctx, v)
@@ -477,26 +475,25 @@ private def evalLazyEntry (config : WhnfCoreConfig)
 This evaluates all lazy entries in a trie and updates `values`, `starIdx`, and `children`
 accordingly.
 -/
-private partial def evalLazyEntries (config : WhnfCoreConfig)
+private partial def evalLazyEntries
     (values : Array α) (starIdx : TrieIndex) (children : Std.HashMap Key TrieIndex)
     (entries : Array (LazyEntry α)) :
     MatchM α (Array α × TrieIndex × Std.HashMap Key TrieIndex) := do
   let mut values := values
   let mut starIdx := starIdx
   let mut children := children
-  entries.foldlM (init := (values, starIdx, children)) (evalLazyEntry config)
+  entries.foldlM (init := (values, starIdx, children)) evalLazyEntry
 
 private def evalNode (c : TrieIndex) :
     MatchM α (Array α × TrieIndex × Std.HashMap Key TrieIndex) := do
   let .node vs star cs pending := (←get).get! c
   if pending.size = 0 then
-    pure (vs, star, cs)
+    return (vs, star, cs)
   else
-    let config ← read
     setTrie c default
-    let (vs, star, cs) ← evalLazyEntries config vs star cs pending
+    let (vs, star, cs) ← evalLazyEntries vs star cs pending
     setTrie c <| .node vs star cs #[]
-    pure (vs, star, cs)
+    return (vs, star, cs)
 
 def dropKeyAux (next : TrieIndex) (rest : List Key) :
     MatchM α Unit :=
@@ -723,11 +720,11 @@ private def push (d : PreDiscrTree α) (k : Key) (e : LazyEntry α) : PreDiscrTr
   d.modifyAt k (·.push e)
 
 /-- Convert a pre-discrimination tree to a lazy discrimination tree. -/
-private def toLazy (d : PreDiscrTree α) (config : WhnfCoreConfig := {}) : LazyDiscrTree α :=
+private def toLazy (d : PreDiscrTree α) : LazyDiscrTree α :=
   let { roots, tries } := d
   -- Adjust trie indices so the first value is reserved (so 0 is never a valid trie index)
   let roots := roots.fold (init := roots) (fun m k n => m.insert k (n+1))
-  { config, roots, tries := #[default] ++ tries.map (.node {} 0 {}) }
+  { roots, tries := #[default] ++ tries.map (.node {} 0 {}) }
 
 /-- Merge two discrimination trees. -/
 protected def append (x y : PreDiscrTree α) : PreDiscrTree α :=
@@ -756,12 +753,12 @@ namespace InitEntry
 /--
 Constructs an initial entry from an expression and value.
 -/
-def fromExpr (expr : Expr) (value : α) (config : WhnfCoreConfig := {}) : MetaM (InitEntry α) := do
+def fromExpr (expr : Expr) (value : α) : MetaM (InitEntry α) := do
   let lctx ← getLCtx
   let linst ← getLocalInstances
   let lctx := (lctx, linst)
-  let (key, todo) ← LazyDiscrTree.rootKey config expr
-  pure <| { key, entry := (todo, lctx, value) }
+  let (key, todo) ← LazyDiscrTree.rootKey expr
+  return { key, entry := (todo, lctx, value) }
 
 /--
 Creates an entry for a subterm of an initial entry.
@@ -769,11 +766,11 @@ Creates an entry for a subterm of an initial entry.
 This is slightly more efficient than using `fromExpr` on subterms since it avoids a redundant call
 to `whnf`.
 -/
-def mkSubEntry (e : InitEntry α) (idx : Nat) (value : α) (config : WhnfCoreConfig := {}) :
+def mkSubEntry (e : InitEntry α) (idx : Nat) (value : α) :
     MetaM (InitEntry α) := do
   let (todo, lctx, _) := e.entry
-  let (key, todo) ← LazyDiscrTree.rootKey config todo[idx]!
-  pure <| { key, entry := (todo, lctx, value) }
+  let (key, todo) ← LazyDiscrTree.rootKey todo[idx]!
+  return { key, entry := (todo, lctx, value) }
 
 end InitEntry
 

src/Lean/Meta/SynthInstance.lean

@@ -207,7 +207,7 @@ def getInstances (type : Expr) : MetaM (Array Instance) := do
     | none   => throwError "type class instance expected{indentExpr type}"
     | some className =>
       let globalInstances ← getGlobalInstancesIndex
-      let result ← globalInstances.getUnify type tcDtConfig
+      let result ← globalInstances.getUnify type
       -- Using insertion sort because it is stable and the array `result` should be mostly sorted.
       -- Most instances have default priority.
       let result := result.insertionSort fun e₁ e₂ => e₁.priority < e₂.priority

src/Lean/Meta/Tactic/FunInd.lean

@@ -776,7 +776,8 @@ In the type of `value`, reduces
 and then wraps `value` in an appropriate type hint.
 -/
 def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
-  let t ← Meta.transform (← inferType value) (skipConstInApp := true) (pre := fun e => do
+  let type ← inferType value
+  let cleanType ← Meta.transform type (skipConstInApp := true) (pre := fun e => do
     -- Need to beta-reduce first
     let e' := e.headBeta
     if e' != e then
@@ -819,7 +820,7 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
           return .continue e'
 
     return .continue e)
-  mkExpectedTypeHint value t
+  mkExpectedTypeHint value cleanType
 
 /--
 Takes `foo._unary.induct`, where the motive is a `PSigma`/`PSum` type and

src/Lean/Meta/Tactic/Injection.lean

@@ -114,10 +114,11 @@ where
         if lhs.isRawNatLit && rhs.isRawNatLit then cont
         else
           try
-            match (← injection mvarId fvarId newNames) with
-            | .solved  => return .solved
-            | .subgoal mvarId newEqs remainingNames =>
-              mvarId.withContext <| go d (newEqs.toList ++ fvarIds) mvarId remainingNames
+            commitIfNoEx do
+              match (← injection mvarId fvarId newNames) with
+              | .solved  => return .solved
+              | .subgoal mvarId newEqs remainingNames =>
+                mvarId.withContext <| go d (newEqs.toList ++ fvarIds) mvarId remainingNames
           catch _ => cont
       else cont
 

src/Lean/Meta/Tactic/Replace.lean

@@ -33,17 +33,21 @@ def _root_.Lean.MVarId.replaceTargetEq (mvarId : MVarId) (targetNew : Expr) (eqP
     return mvarNew.mvarId!
 
 /--
-  Convert the given goal `Ctx |- target` into `Ctx |- targetNew`. It assumes the goals are definitionally equal.
-  We use the proof term
-  ```
-  @id target mvarNew
-  ```
-  to create a checkpoint. -/
+Converts the given goal `Ctx |- target` into `Ctx |- targetNew`. It assumes the goals are definitionally equal.
+We use the proof term
+```
+@id target mvarNew
+```
+to create a checkpoint.
+
+If `targetNew` is equal to `target`, then returns `mvarId` unchanged.
+Uses `Expr.equal` for the comparison so that it is possible to update binder names, etc., which are user-visible.
+-/
 def _root_.Lean.MVarId.replaceTargetDefEq (mvarId : MVarId) (targetNew : Expr) : MetaM MVarId :=
   mvarId.withContext do
     mvarId.checkNotAssigned `change
     let target  ← mvarId.getType
-    if target == targetNew then
+    if Expr.equal target targetNew then
       return mvarId
     else
       let tag     ← mvarId.getTag
@@ -95,12 +99,15 @@ abbrev _root_.Lean.MVarId.replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (
   replaceLocalDeclCore mvarId fvarId typeNew eqProof
 
 /--
-Replace the type of `fvarId` at `mvarId` with `typeNew`.
+Replaces the type of `fvarId` at `mvarId` with `typeNew`.
 Remark: this method assumes that `typeNew` is definitionally equal to the current type of `fvarId`.
+
+If `typeNew` is equal to current type of `fvarId`, then returns `mvarId` unchanged.
+Uses `Expr.equal` for the comparison so that it is possible to update binder names, etc., which are user-visible.
 -/
 def _root_.Lean.MVarId.replaceLocalDeclDefEq (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) : MetaM MVarId := do
   mvarId.withContext do
-    if typeNew == (← fvarId.getType) then
+    if Expr.equal typeNew (← fvarId.getType) then
       return mvarId
     else
       let mvarDecl ← mvarId.getDecl

src/Lean/Meta/Tactic/Rfl.lean

@@ -19,9 +19,6 @@ namespace Lean.Meta.Rfl
 
 open Lean Meta
 
-/-- Discrimation tree settings for the `refl` extension. -/
-def reflExt.config : WhnfCoreConfig := {}
-
 /-- Environment extensions for `refl` lemmas -/
 initialize reflExt :
     SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ←
@@ -42,7 +39,7 @@ initialize registerBuiltinAttribute {
     if let .app (.const ``Eq [_]) _ := rel then
       throwError "@[refl] attribute may not be used on `Eq.refl`."
     unless ← withNewMCtxDepth <| isDefEq lhs rhs do fail
-    let key ← DiscrTree.mkPath rel reflExt.config
+    let key ← DiscrTree.mkPath rel
     reflExt.add (decl, key) kind
 }
 
@@ -91,7 +88,7 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
     goal.setType (.app t.appFn! lhs)
     let s ← saveState
     let mut ex? := none
-    for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
+    for lem in ← (reflExt.getState (← getEnv)).getMatch rel do
       try
         let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
         if gs.isEmpty then return () else
@@ -123,7 +120,7 @@ def _root_.Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM MVarId := do
   if rel.isAppOf `Eq then
     -- No need to lift Eq to Eq
     return mvarId
-  for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
+  for lem in ← (reflExt.getState (← getEnv)).getMatch rel do
     let res ← observing? do
       -- First create an equality relating the LHS and RHS
       -- and reduce the goal to proving that LHS is related to LHS.

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

@@ -239,9 +239,10 @@ def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
     withFreshCache do
       let mut s ← getSimpTheorems
       let mut updated := false
+      let ctx ← getContext
       for x in xs do
         if (← isProof x) then
-          s ← s.addTheorem (.fvar x.fvarId!) x
+          s ← s.addTheorem (.fvar x.fvarId!) x (config := ctx.indexConfig)
           updated := true
       if updated then
         withSimpTheorems s f
@@ -832,7 +833,7 @@ def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsAr
   for h in (← getPropHyps) do
     let localDecl ← h.getDecl
     let proof  := localDecl.toExpr
-    let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof
+    let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof (config := ctx.indexConfig)
     ctx := ctx.setSimpTheorems simpTheorems
   match (← simpTarget mvarId ctx simprocs discharge? (stats := stats)) with
   | (none, stats) => return (TacticResultCNM.closed, stats)

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

@@ -203,7 +203,7 @@ def rewrite? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (tag :
 where
   /-- For `(← getConfig).index := true`, use discrimination tree structure when collecting `simp` theorem candidates. -/
   rewriteUsingIndex? : SimpM (Option Result) := do
-    let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
+    let candidates ← withSimpIndexConfig <| s.getMatchWithExtra e
     if candidates.isEmpty then
       trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"
       return none
@@ -221,7 +221,7 @@ where
   Only the root symbol is taken into account. Most of the structure of the discrimination tree is ignored.
   -/
   rewriteNoIndex? : SimpM (Option Result) := do
-    let (candidates, numArgs) ← s.getMatchLiberal e (getDtConfig (← getConfig))
+    let (candidates, numArgs) ← withSimpIndexConfig <| s.getMatchLiberal e
     if candidates.isEmpty then
       trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"
       return none
@@ -245,7 +245,7 @@ where
 
   diagnoseWhenNoIndex (thm : SimpTheorem) : SimpM Unit := do
     if (← isDiagnosticsEnabled) then
-      let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
+      let candidates ← withSimpIndexConfig <| s.getMatchWithExtra e
       for (candidate, _) in candidates do
         if unsafe ptrEq thm candidate then
           return ()

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

@@ -42,7 +42,8 @@ private def initEntries : M Unit := do
     unless simpThms.isErased (.fvar h) do
       let localDecl ← h.getDecl
       let proof  := localDecl.toExpr
-      simpThms ← simpThms.addTheorem (.fvar h) proof
+      let ctx := (← get).ctx
+      simpThms ← simpThms.addTheorem (.fvar h) proof (config := ctx.indexConfig)
       modify fun s => { s with ctx := s.ctx.setSimpTheorems simpThms }
       if hsNonDeps.contains h then
         -- We only simplify nondependent hypotheses
@@ -95,7 +96,7 @@ private partial def loop : M Bool := do
         trace[Meta.Tactic.simp.all] "entry.id: {← ppOrigin entry.id}, {entry.type} => {typeNew}"
         let mut simpThmsNew := (← getSimpTheorems).eraseTheorem (.fvar entry.fvarId)
         let idNew ← mkFreshId
-        simpThmsNew ← simpThmsNew.addTheorem (.other idNew) (← mkExpectedTypeHint proofNew typeNew)
+        simpThmsNew ← simpThmsNew.addTheorem (.other idNew) (← mkExpectedTypeHint proofNew typeNew) (config := ctx.indexConfig)
         modify fun s => { s with
           modified         := true
           ctx              := ctx.setSimpTheorems simpThmsNew

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

@@ -204,8 +204,18 @@ structure SimpTheorems where
   toUnfoldThms : PHashMap Name (Array Name) := {}
   deriving Inhabited
 
-/-- Configuration for the discrimination tree. -/
-def simpDtConfig : WhnfCoreConfig := { iota := false, proj := .no, zetaDelta := false }
+/--
+Configuration for `MetaM` used to process global simp theorems
+-/
+def simpGlobalConfig : ConfigWithKey :=
+  { iota         := false
+    proj         := .no
+    zetaDelta    := false
+    transparency := .reducible
+  : Config }.toConfigWithKey
+
+@[inline] def withSimpGlobalConfig : MetaM α → MetaM α :=
+  withConfigWithKey simpGlobalConfig
 
 partial def SimpTheorems.eraseCore (d : SimpTheorems) (thmId : Origin) : SimpTheorems :=
   let d := { d with erased := d.erased.insert thmId, lemmaNames := d.lemmaNames.erase thmId }
@@ -298,7 +308,7 @@ private partial def isPerm : Expr → Expr → MetaM Bool
   | s, t => return s == t
 
 private def checkBadRewrite (lhs rhs : Expr) : MetaM Unit := do
-  let lhs ← DiscrTree.reduceDT lhs (root := true) simpDtConfig
+  let lhs ← withSimpGlobalConfig <| DiscrTree.reduceDT lhs (root := true)
   if lhs == rhs && lhs.isFVar then
     throwError "invalid `simp` theorem, equation is equivalent to{indentExpr (← mkEq lhs rhs)}"
 
@@ -381,11 +391,11 @@ private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array
   assert! origin != .fvar ⟨.anonymous⟩
   let type ← instantiateMVars (← inferType e)
   withNewMCtxDepth do
-    let (_, _, type) ← withReducible <| forallMetaTelescopeReducing type
+    let (_, _, type) ← forallMetaTelescopeReducing type
     let type ← whnfR type
     let (keys, perm) ←
       match type.eq? with
-      | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs simpDtConfig noIndexAtArgs, ← isPerm lhs rhs)
+      | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs noIndexAtArgs, ← isPerm lhs rhs)
       | none => throwError "unexpected kind of 'simp' theorem{indentExpr type}"
     return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl := (← isRflProof proof) }
 
@@ -394,7 +404,7 @@ private def mkSimpTheoremsFromConst (declName : Name) (post : Bool) (inv : Bool)
   let us := cinfo.levelParams.map mkLevelParam
   let origin := .decl declName post inv
   let val := mkConst declName us
-  withReducible do
+  withSimpGlobalConfig do
     let type ← inferType val
     checkTypeIsProp type
     if inv || (← shouldPreprocess type) then
@@ -464,18 +474,10 @@ private def preprocessProof (val : Expr) (inv : Bool) : MetaM (Array Expr) := do
   return ps.toArray.map fun (val, _) => val
 
 /-- Auxiliary method for creating simp theorems from a proof term `val`. -/
-def mkSimpTheorems (id : Origin) (levelParams : Array Name) (proof : Expr) (post := true) (inv := false) (prio : Nat := eval_prio default) : MetaM (Array SimpTheorem) :=
+private def mkSimpTheorems (id : Origin) (levelParams : Array Name) (proof : Expr) (post := true) (inv := false) (prio : Nat := eval_prio default) : MetaM (Array SimpTheorem) :=
   withReducible do
     (← preprocessProof proof inv).mapM fun val => mkSimpTheoremCore id val levelParams val post prio (noIndexAtArgs := true)
 
-/-- Auxiliary method for adding a local simp theorem to a `SimpTheorems` datastructure. -/
-def SimpTheorems.add (s : SimpTheorems) (id : Origin) (levelParams : Array Name) (proof : Expr) (inv := false) (post := true) (prio : Nat := eval_prio default) : MetaM SimpTheorems := do
-  if proof.isConst then
-    s.addConst proof.constName! post inv prio
-  else
-    let simpThms ← mkSimpTheorems id levelParams proof post inv prio
-    return simpThms.foldl addSimpTheoremEntry s
-
 /--
 Reducible functions and projection functions should always be put in `toUnfold`, instead
 of trying to use equational theorems.
@@ -533,14 +535,25 @@ def SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM Si
   else
     return d.addDeclToUnfoldCore declName
 
+/-- Auxiliary method for adding a local simp theorem to a `SimpTheorems` datastructure. -/
+def SimpTheorems.add (s : SimpTheorems) (id : Origin) (levelParams : Array Name) (proof : Expr)
+        (inv := false) (post := true) (prio : Nat := eval_prio default)
+        (config : ConfigWithKey := simpGlobalConfig) : MetaM SimpTheorems := do
+  if proof.isConst then
+    -- Recall that we use `simpGlobalConfig` for processing global declarations.
+    s.addConst proof.constName! post inv prio
+  else
+    let simpThms ← withConfigWithKey config <| mkSimpTheorems id levelParams proof post inv prio
+    return simpThms.foldl addSimpTheoremEntry s
+
 abbrev SimpTheoremsArray := Array SimpTheorems
 
-def SimpTheoremsArray.addTheorem (thmsArray : SimpTheoremsArray) (id : Origin) (h : Expr) : MetaM SimpTheoremsArray :=
+def SimpTheoremsArray.addTheorem (thmsArray : SimpTheoremsArray) (id : Origin) (h : Expr) (config : ConfigWithKey := simpGlobalConfig) : MetaM SimpTheoremsArray :=
   if thmsArray.isEmpty then
     let thms : SimpTheorems := {}
-    return #[ (← thms.add id #[] h) ]
+    return #[ (← thms.add id #[] h (config := config)) ]
   else
-    thmsArray.modifyM 0 fun thms => thms.add id #[] h
+    thmsArray.modifyM 0 fun thms => thms.add id #[] h (config := config)
 
 def SimpTheoremsArray.eraseTheorem (thmsArray : SimpTheoremsArray) (thmId : Origin) : SimpTheoremsArray :=
   thmsArray.map fun thms => thms.eraseCore thmId

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

@@ -213,7 +213,7 @@ def SimprocEntry.tryD (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM
   | .inr proc => return (← proc e).addExtraArgs extraArgs
 
 def simprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM Step := do
-  let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
+  let candidates ← withSimpIndexConfig <| s.getMatchWithExtra e
   if candidates.isEmpty then
     let tag := if post then "post" else "pre"
     trace[Debug.Meta.Tactic.simp] "no {tag}-simprocs found for {e}"
@@ -250,7 +250,7 @@ def simprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Ex
       return .continue
 
 def dsimprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM DStep := do
-  let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
+  let candidates ← withSimpIndexConfig <| s.getMatchWithExtra e
   if candidates.isEmpty then
     let tag := if post then "post" else "pre"
     trace[Debug.Meta.Tactic.simp] "no {tag}-simprocs found for {e}"

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

@@ -53,7 +53,9 @@ abbrev CongrCache := ExprMap (Option CongrTheorem)
 
 structure Context where
   private mk ::
-  config           : Config := {}
+  config            : Config := {}
+  metaConfig        : ConfigWithKey := default
+  indexConfig       : ConfigWithKey := default
   /-- `maxDischargeDepth` from `config` as an `UInt32`. -/
   maxDischargeDepth : UInt32 := UInt32.ofNatTruncate config.maxDischargeDepth
   simpTheorems      : SimpTheoremsArray := {}
@@ -117,9 +119,32 @@ private def updateArith (c : Config) : CoreM Config := do
   else
     return c
 
+/--
+Converts `Simp.Config` into `Meta.ConfigWithKey` used for indexing.
+-/
+private def mkIndexConfig (c : Config) : ConfigWithKey :=
+  { c with
+    proj         := .no
+    transparency := .reducible
+  : Meta.Config }.toConfigWithKey
+
+/--
+Converts `Simp.Config` into `Meta.ConfigWithKey` used for `isDefEq`.
+-/
+-- TODO: use `metaConfig` at `isDefEq`. It is not being used yet because it will break Mathlib.
+private def mkMetaConfig (c : Config) : ConfigWithKey :=
+  { c with
+    proj         := if c.proj then .yesWithDelta else .no
+    transparency := .reducible
+  : Meta.Config }.toConfigWithKey
+
 def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (congrTheorems : SimpCongrTheorems := {}) : MetaM Context := do
   let config ← updateArith config
-  return { config, simpTheorems, congrTheorems }
+  return {
+    config, simpTheorems, congrTheorems
+    metaConfig := mkMetaConfig config
+    indexConfig := mkIndexConfig config
+  }
 
 def Context.setConfig (context : Context) (config : Config) : Context :=
   { context with config }
@@ -203,6 +228,15 @@ abbrev SimpM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
 @[inline] def withInDSimp : SimpM α → SimpM α :=
   withTheReader Context (fun ctx => { ctx with inDSimp := true })
 
+/--
+Executes `x` using a `MetaM` configuration for indexing terms.
+It is inferred from `Simp.Config`.
+For example, if the user has set `simp (config := { zeta := false })`,
+`isDefEq` and `whnf` in `MetaM` should not perform `zeta` reduction.
+-/
+@[inline] def withSimpIndexConfig (x : SimpM α) : SimpM α := do
+  withConfigWithKey (← readThe Simp.Context).indexConfig x
+
 @[extern "lean_simp"]
 opaque simp (e : Expr) : SimpM Result
 
@@ -679,16 +713,6 @@ def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
     /- See comment above. This is reachable if `hasCast == true`. The `rhs` is not structurally equal to `mkAppN f argsNew` -/
     return some { expr := rhs }
 
-/--
-Return a WHNF configuration for retrieving `[simp]` from the discrimination tree.
-If user has disabled `zeta` and/or `beta` reduction in the simplifier, or enabled `zetaDelta`,
-we must also disable/enable them when retrieving lemmas from discrimination tree. See issues: #2669 and #2281
--/
-def getDtConfig (cfg : Config) : WhnfCoreConfig :=
-  match cfg.beta, cfg.zeta, cfg.zetaDelta with
-  | true, true, false => simpDtConfig
-  | _,    _,    _     => { simpDtConfig with zeta := cfg.zeta, beta := cfg.beta, zetaDelta := cfg.zetaDelta }
-
 def Result.addExtraArgs (r : Result) (extraArgs : Array Expr) : MetaM Result := do
   match r.proof? with
   | none => return { expr := mkAppN r.expr extraArgs }

src/Lean/Meta/Tactic/Symm.lean

@@ -18,9 +18,6 @@ open Lean Meta
 
 namespace Lean.Meta.Symm
 
-/-- Discrimation tree settings for the `symm` extension. -/
-def symmExt.config : WhnfCoreConfig := {}
-
 /-- Environment extensions for symm lemmas -/
 builtin_initialize symmExt :
     SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ←
@@ -40,7 +37,7 @@ builtin_initialize registerBuiltinAttribute {
     let some _ := xs.back? | fail
     let targetTy ← reduce targetTy
     let .app (.app rel _) _ := targetTy | fail
-    let key ← withReducible <| DiscrTree.mkPath rel symmExt.config
+    let key ← withReducible <| DiscrTree.mkPath rel
     symmExt.add (decl, key) kind
 }
 
@@ -54,7 +51,7 @@ namespace Lean.Expr
 def getSymmLems (tgt : Expr) : MetaM (Array Name) := do
   let .app (.app rel _) _ := tgt
     | throwError "symmetry lemmas only apply to binary relations, not{indentExpr tgt}"
-  (symmExt.getState (← getEnv)).getMatch rel symmExt.config
+  (symmExt.getState (← getEnv)).getMatch rel
 
 /-- Given a term `e : a ~ b`, construct a term in `b ~ a` using `@[symm]` lemmas. -/
 def applySymm (e : Expr) : MetaM Expr := do

src/Lean/Meta/UnificationHint.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.ScopedEnvExtension
 import Lean.Util.Recognizers
+import Lean.Meta.Basic
 import Lean.Meta.DiscrTree
 import Lean.Meta.SynthInstance
 
@@ -27,7 +28,8 @@ structure UnificationHints where
 instance : ToFormat UnificationHints where
   format h := format h.discrTree
 
-def UnificationHints.config : WhnfCoreConfig := { iota := false, proj := .no }
+private def config : ConfigWithKey :=
+  { iota := false, proj := .no : Config }.toConfigWithKey
 
 def UnificationHints.add (hints : UnificationHints) (e : UnificationHintEntry) : UnificationHints :=
   { hints with discrTree := hints.discrTree.insertCore e.keys e.val }
@@ -81,7 +83,7 @@ def addUnificationHint (declName : Name) (kind : AttributeKind) : MetaM Unit :=
       match decodeUnificationHint body with
       | Except.error msg => throwError msg
       | Except.ok hint =>
-        let keys ← DiscrTree.mkPath hint.pattern.lhs UnificationHints.config
+        let keys ← withConfigWithKey config <| DiscrTree.mkPath hint.pattern.lhs
         validateHint hint
         unificationHintExtension.add { keys := keys, val := declName } kind
 
@@ -101,7 +103,7 @@ def tryUnificationHints (t s : Expr) : MetaM Bool := do
   if t.isMVar then
     return false
   let hints := unificationHintExtension.getState (← getEnv)
-  let candidates ← hints.discrTree.getMatch t UnificationHints.config
+  let candidates ← withConfigWithKey config <| hints.discrTree.getMatch t
   for candidate in candidates do
     if (← tryCandidate candidate) then
       return true

src/Lean/Meta/WHNF.lean

@@ -328,65 +328,8 @@ end
 /-! # Weak Head Normal Form auxiliary combinators -/
 -- ===========================
 
-/--
-Configuration for projection reduction. See `whnfCore`.
--/
-inductive ProjReductionKind where
-  /-- Projections `s.i` are not reduced at `whnfCore`. -/
-  | no
-  /--
-  Projections `s.i` are reduced at `whnfCore`, and `whnfCore` is used at `s` during the process.
-  Recall that `whnfCore` does not perform `delta` reduction (i.e., it will not unfold constant declarations).
-  -/
-  | yes
-  /--
-  Projections `s.i` are reduced at `whnfCore`, and `whnf` is used at `s` during the process.
-  Recall that `whnfCore` does not perform `delta` reduction (i.e., it will not unfold constant declarations), but `whnf` does.
-  -/
-  | yesWithDelta
-  /--
-  Projections `s.i` are reduced at `whnfCore`, and `whnfAtMostI` is used at `s` during the process.
-  Recall that `whnfAtMostI` is like `whnf` but uses transparency at most `instances`.
-  This option is stronger than `yes`, but weaker than `yesWithDelta`.
-  We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations.
-  When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`,
-  we only want to unify negation (and not all other field operations as well).
-  Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986
-  -/
-  | yesWithDeltaI
-  deriving DecidableEq, Inhabited, Repr
-
-/--
-Configuration options for `whnfEasyCases` and `whnfCore`.
--/
-structure WhnfCoreConfig where
-  /-- If `true`, reduce recursor/matcher applications, e.g., `Nat.rec true (fun _ _ => false) Nat.zero` reduces to `true` -/
-  iota : Bool := true
-  /-- If `true`, reduce terms such as `(fun x => t[x]) a` into `t[a]` -/
-  beta : Bool := true
-  /-- Control projection reduction at `whnfCore`. -/
-  proj : ProjReductionKind := .yesWithDelta
-  /--
-  Zeta reduction: `let x := v; e[x]` reduces to `e[v]`.
-  We say a let-declaration `let x := v; e` is non dependent if it is equivalent to `(fun x => e) v`.
-  Recall that
-  ```
-  fun x : BitVec 5 => let n := 5; fun y : BitVec n => x = y
-  ```
-  is type correct, but
-  ```
-  fun x : BitVec 5 => (fun n => fun y : BitVec n => x = y) 5
-  ```
-  is not.
-  -/
-  zeta : Bool := true
-  /--
-  Zeta-delta reduction: given a local context containing entry `x : t := e`, free variable `x` reduces to `e`.
-  -/
-  zetaDelta : Bool := true
-
 /-- Auxiliary combinator for handling easy WHNF cases. It takes a function for handling the "hard" cases as an argument -/
-@[specialize] partial def whnfEasyCases (e : Expr) (k : Expr → MetaM Expr) (config : WhnfCoreConfig := {}) : MetaM Expr := do
+@[specialize] partial def whnfEasyCases (e : Expr) (k : Expr → MetaM Expr) : MetaM Expr := do
   match e with
   | .forallE ..    => return e
   | .lam ..        => return e
@@ -397,7 +340,7 @@ structure WhnfCoreConfig where
   | .const ..      => k e
   | .app ..        => k e
   | .proj ..       => k e
-  | .mdata _ e     => whnfEasyCases e k config
+  | .mdata _ e     => whnfEasyCases e k
   | .fvar fvarId   =>
     let decl ← fvarId.getDecl
     match decl with
@@ -405,13 +348,14 @@ structure WhnfCoreConfig where
     | .ldecl (value := v) .. =>
       -- Let-declarations marked as implementation detail should always be unfolded
       -- We initially added this feature for `simp`, and added it here for consistency.
-      unless config.zetaDelta || decl.isImplementationDetail do return e
-      if (← getConfig).trackZetaDelta then
+      let cfg ← getConfig
+      unless cfg.zetaDelta || decl.isImplementationDetail do return e
+      if cfg.trackZetaDelta then
         modify fun s => { s with zetaDeltaFVarIds := s.zetaDeltaFVarIds.insert fvarId }
-      whnfEasyCases v k config
+      whnfEasyCases v k
   | .mvar mvarId   =>
     match (← getExprMVarAssignment? mvarId) with
-    | some v => whnfEasyCases v k config
+    | some v => whnfEasyCases v k
     | none   => return e
 
 @[specialize] private def deltaDefinition (c : ConstantInfo) (lvls : List Level)
@@ -611,30 +555,31 @@ private def whnfDelayedAssigned? (f' : Expr) (e : Expr) : MetaM (Option Expr) :=
 Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
 expand let-expressions, expand assigned meta-variables.
 -/
-partial def whnfCore (e : Expr) (config : WhnfCoreConfig := {}): MetaM Expr :=
+partial def whnfCore (e : Expr) : MetaM Expr :=
   go e
 where
   go (e : Expr) : MetaM Expr :=
-    whnfEasyCases e (config := config) fun e => do
+    whnfEasyCases e fun e => do
       trace[Meta.whnf] e
       match e with
       | .const ..  => pure e
-      | .letE _ _ v b _ => if config.zeta then go <| b.instantiate1 v else return e
+      | .letE _ _ v b _ => if (← getConfig).zeta then go <| b.instantiate1 v else return e
       | .app f ..       =>
-        if config.zeta then
+        let cfg ← getConfig
+        if cfg.zeta then
           if let some (args, _, _, v, b) := e.letFunAppArgs? then
             -- When zeta reducing enabled, always reduce `letFun` no matter the current reducibility level
             return (← go <| mkAppN (b.instantiate1 v) args)
         let f := f.getAppFn
         let f' ← go f
-        if config.beta && f'.isLambda then
+        if cfg.beta && f'.isLambda then
           let revArgs := e.getAppRevArgs
           go <| f'.betaRev revArgs
         else if let some eNew ← whnfDelayedAssigned? f' e then
           go eNew
         else
           let e := if f == f' then e else e.updateFn f'
-          unless config.iota do return e
+          unless cfg.iota do return e
           match (← reduceMatcher? e) with
           | .reduced eNew => go eNew
           | .partialApp   => pure e
@@ -656,7 +601,7 @@ where
           match (← projectCore? c i) with
           | some e => go e
           | none => return e
-        match config.proj with
+        match (← getConfig).proj with
         | .no => return e
         | .yes => k (← go c)
         | .yesWithDelta => k (← whnf c)
@@ -967,26 +912,18 @@ def reduceNat? (e : Expr) : MetaM (Option Expr) :=
   if e.hasFVar || e.hasExprMVar || (← read).canUnfold?.isSome then
     return false
   else
-    match (← getConfig).transparency with
-    | .default => return true
-    | .all     => return true
-    | _        => return false
+    return true
 
 @[inline] private def cached? (useCache : Bool) (e : Expr) : MetaM (Option Expr) := do
   if useCache then
-    match (← getConfig).transparency with
-    | .default => return (← get).cache.whnfDefault.find? e
-    | .all     => return (← get).cache.whnfAll.find? e
-    | _        => unreachable!
+    return (← get).cache.whnf.find? (← mkExprConfigCacheKey e)
   else
     return none
 
 private def cache (useCache : Bool) (e r : Expr) : MetaM Expr := do
   if useCache then
-    match (← getConfig).transparency with
-    | .default => modify fun s => { s with cache.whnfDefault := s.cache.whnfDefault.insert e r }
-    | .all     => modify fun s => { s with cache.whnfAll     := s.cache.whnfAll.insert e r }
-    | _        => unreachable!
+    let key ← mkExprConfigCacheKey e
+    modify fun s => { s with cache.whnf := s.cache.whnf.insert key r }
   return r
 
 @[export lean_whnf]

src/Lean/MetavarContext.lean

@@ -1219,7 +1219,7 @@ private def mkLambda' (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) (etaRed
   Similar to `LocalContext.mkBinding`, but handles metavariables correctly.
   If `usedOnly == true` then `forall` and `lambda` expressions are created only for used variables.
   If `usedLetOnly == true` then `let` expressions are created only for used (let-) variables. -/
-@[specialize] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) (usedOnly : Bool) (usedLetOnly : Bool) (etaReduce : Bool) : M Expr := do
+def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) (usedOnly : Bool) (usedLetOnly : Bool) (etaReduce : Bool) : M Expr := do
   let e ← abstractRange xs xs.size e
   xs.size.foldRevM (init := e) fun i e => do
       let x := xs[i]!

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -24,6 +24,11 @@ register_builtin_option pp.notation : Bool := {
   group    := "pp"
   descr    := "(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)"
 }
+register_builtin_option pp.parens : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) if set to true, notation is wrapped in parentheses regardless of precedence"
+}
 register_builtin_option pp.unicode.fun : Bool := {
   defValue := false
   group    := "pp"
@@ -248,6 +253,7 @@ def getPPNatLit (o : Options) : Bool := o.get pp.natLit.name (getPPNumericTypes
 def getPPCoercions (o : Options) : Bool := o.get pp.coercions.name (!getPPAll o)
 def getPPExplicit (o : Options) : Bool := o.get pp.explicit.name (getPPAll o)
 def getPPNotation (o : Options) : Bool := o.get pp.notation.name (!getPPAll o)
+def getPPParens (o : Options) : Bool := o.get pp.parens.name pp.parens.defValue
 def getPPUnicodeFun (o : Options) : Bool := o.get pp.unicode.fun.name false
 def getPPMatch (o : Options) : Bool := o.get pp.match.name (!getPPAll o)
 def getPPFieldNotation (o : Options) : Bool := o.get pp.fieldNotation.name (!getPPAll o)

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -8,6 +8,7 @@ import Lean.Parser.Extension
 import Lean.Parser.StrInterpolation
 import Lean.ParserCompiler.Attribute
 import Lean.PrettyPrinter.Basic
+import Lean.PrettyPrinter.Delaborator.Options
 
 
 /-!
@@ -82,8 +83,10 @@ namespace PrettyPrinter
 namespace Parenthesizer
 
 structure Context where
-  -- We need to store this `categoryParser` argument to deal with the implicit Pratt parser call in `trailingNode.parenthesizer`.
+  /-- We need to store this `categoryParser` argument to deal with the implicit Pratt parser call in `trailingNode.parenthesizer`. -/
   cat : Name := Name.anonymous
+  /-- Whether to add parentheses regardless of any other conditions. This is cached from the `pp.parens` option. -/
+  forceParens : Bool := false
 
 structure State where
   stxTrav : Syntax.Traverser
@@ -217,8 +220,13 @@ def maybeParenthesize (cat : Name) (canJuxtapose : Bool) (mkParen : Syntax → S
   let { minPrec := some minPrec, trailPrec := trailPrec, trailCat := trailCat, .. } ← get
     | trace[PrettyPrinter.parenthesize] "visited a syntax tree without precedences?!{line ++ format stx}"
   trace[PrettyPrinter.parenthesize] (m!"...precedences are {prec} >? {minPrec}" ++ if canJuxtapose then m!", {(trailPrec, trailCat)} <=? {(st.contPrec, st.contCat)}" else "")
-  -- Should we parenthesize?
-  if (prec > minPrec || canJuxtapose && match trailPrec, st.contPrec with | some trailPrec, some contPrec => trailCat == st.contCat && trailPrec <= contPrec | _, _ => false) then
+  /- Should we parenthesize?
+     * Note about forceParens mode: we don't insert outermost parentheses (we use the syntax traverser parents to detect this),
+       and we don't insert parentheses when we are at `maxPrec` (since this is effectively infinity).
+  -/
+  if (((← read).forceParens && !st.stxTrav.parents.isEmpty && minPrec < Parser.maxPrec)
+      || prec > minPrec
+      || canJuxtapose && match trailPrec, st.contPrec with | some trailPrec, some contPrec => trailCat == st.contCat && trailPrec <= contPrec | _, _ => false) then
       -- The recursive `visit` call, by the invariant, has moved to the preceding node. In order to parenthesize
       -- the original node, we must first move to the right, except if we already were at the left-most child in the first
       -- place.
@@ -540,16 +548,23 @@ instance : Coe (Parenthesizer → Parenthesizer → Parenthesizer) Parenthesizer
 end Parenthesizer
 open Parenthesizer
 
-/-- Add necessary parentheses in `stx` parsed by `parser`. -/
+/--
+Adds necessary parentheses in `stx` parsed by `parser`.
+-/
 def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : CoreM Syntax := do
   trace[PrettyPrinter.parenthesize.input] "{format stx}"
+  let opts ← getOptions
   catchInternalId backtrackExceptionId
     (do
-      let (_, st) ← (parenthesizer {}).run { stxTrav := Syntax.Traverser.fromSyntax stx }
+      let (_, st) ← (parenthesizer { forceParens := getPPParens opts }).run { stxTrav := Syntax.Traverser.fromSyntax stx }
       pure st.stxTrav.cur)
     (fun _ => throwError "parenthesize: uncaught backtrack exception")
 
-def parenthesizeCategory (cat : Name) := parenthesize <| categoryParser.parenthesizer cat 0
+/--
+Adds necessary parentheses to the syntax in the given category (for example, `term`, `tactic`, or `command`).
+-/
+def parenthesizeCategory (cat : Name) (stx : Syntax) :=
+  parenthesize (categoryParser.parenthesizer cat 0) stx
 
 def parenthesizeTerm := parenthesizeCategory `term
 def parenthesizeTactic := parenthesizeCategory `tactic

src/include/lean/lean.h

@@ -37,7 +37,15 @@ extern "C" {
 #if defined(__GNUC__) || defined(__clang__)
 #define LEAN_UNLIKELY(x) (__builtin_expect((x), 0))
 #define LEAN_LIKELY(x) (__builtin_expect((x), 1))
+
+#ifdef NDEBUG
 #define LEAN_ALWAYS_INLINE __attribute__((always_inline))
+#else
+// We have observed stack frame increases from forced inlining overflowing the stack in debug builds,
+// let's leave the decision to the compiler in that case
+#define LEAN_ALWAYS_INLINE
+#endif
+
 #else
 #define LEAN_UNLIKELY(x) (x)
 #define LEAN_LIKELY(x) (x)
@@ -286,7 +294,7 @@ typedef struct {
     void *                m_data;
 } lean_external_object;
 
-static inline bool lean_is_scalar(lean_object * o) { return ((size_t)(o) & 1) == 1; }
+static inline LEAN_ALWAYS_INLINE bool lean_is_scalar(lean_object * o) { return ((size_t)(o) & 1) == 1; }
 static inline lean_object * lean_box(size_t n) { return (lean_object*)(((size_t)(n) << 1) | 1); }
 static inline size_t lean_unbox(lean_object * o) { return (size_t)(o) >> 1; }
 
@@ -440,16 +448,16 @@ static inline void lean_inc_ref_n(lean_object * o, size_t n) {
 
 LEAN_EXPORT void lean_dec_ref_cold(lean_object * o);
 
-static inline void lean_dec_ref(lean_object * o) {
+static inline LEAN_ALWAYS_INLINE void lean_dec_ref(lean_object * o) {
     if (LEAN_LIKELY(o->m_rc > 1)) {
         o->m_rc--;
     } else if (o->m_rc != 0) {
         lean_dec_ref_cold(o);
     }
 }
-static inline void lean_inc(lean_object * o) { if (!lean_is_scalar(o)) lean_inc_ref(o); }
+static inline void LEAN_ALWAYS_INLINE lean_inc(lean_object * o) { if (!lean_is_scalar(o)) lean_inc_ref(o); }
 static inline void lean_inc_n(lean_object * o, size_t n) { if (!lean_is_scalar(o)) lean_inc_ref_n(o, n); }
-static inline void lean_dec(lean_object * o) { if (!lean_is_scalar(o)) lean_dec_ref(o); }
+static inline void LEAN_ALWAYS_INLINE lean_dec(lean_object * o) { if (!lean_is_scalar(o)) lean_dec_ref(o); }
 
 static inline bool lean_is_ctor(lean_object * o) { return lean_ptr_tag(o) <= LeanMaxCtorTag; }
 static inline bool lean_is_closure(lean_object * o) { return lean_ptr_tag(o) == LeanClosure; }
@@ -1195,14 +1203,14 @@ static inline lean_obj_res lean_nat_succ(b_lean_obj_arg a) {
         return lean_nat_big_succ(a);
 }
 
-static inline lean_obj_res lean_nat_add(b_lean_obj_arg a1, b_lean_obj_arg a2) {
+static inline LEAN_ALWAYS_INLINE lean_obj_res lean_nat_add(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2)))
         return lean_usize_to_nat(lean_unbox(a1) + lean_unbox(a2));
     else
         return lean_nat_big_add(a1, a2);
 }
 
-static inline lean_obj_res lean_nat_sub(b_lean_obj_arg a1, b_lean_obj_arg a2) {
+static inline LEAN_ALWAYS_INLINE lean_obj_res lean_nat_sub(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
         size_t n1 = lean_unbox(a1);
         size_t n2 = lean_unbox(a2);
@@ -1215,7 +1223,7 @@ static inline lean_obj_res lean_nat_sub(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     }
 }
 
-static inline lean_obj_res lean_nat_mul(b_lean_obj_arg a1, b_lean_obj_arg a2) {
+static inline LEAN_ALWAYS_INLINE lean_obj_res lean_nat_mul(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
         size_t n1 = lean_unbox(a1);
         if (n1 == 0)
@@ -1257,7 +1265,7 @@ static inline lean_obj_res lean_nat_mod(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     }
 }
 
-static inline bool lean_nat_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) {
+static inline LEAN_ALWAYS_INLINE bool lean_nat_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
         // This comparison is UB according to the standard but allowed as per the
         // GCC documentation and the address sanitizer does not complain about it.
@@ -1267,7 +1275,7 @@ static inline bool lean_nat_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     }
 }
 
-static inline uint8_t lean_nat_dec_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) {
+static inline LEAN_ALWAYS_INLINE uint8_t lean_nat_dec_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     return lean_nat_eq(a1, a2);
 }
 
@@ -1275,7 +1283,7 @@ static inline bool lean_nat_ne(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     return !lean_nat_eq(a1, a2);
 }
 
-static inline bool lean_nat_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
+static inline LEAN_ALWAYS_INLINE bool lean_nat_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
         // This comparison is UB according to the standard but allowed as per the
         // GCC documentation and the address sanitizer does not complain about it.
@@ -1285,11 +1293,11 @@ static inline bool lean_nat_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     }
 }
 
-static inline uint8_t lean_nat_dec_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
+static inline LEAN_ALWAYS_INLINE uint8_t lean_nat_dec_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     return lean_nat_le(a1, a2);
 }
 
-static inline bool lean_nat_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
+static inline LEAN_ALWAYS_INLINE bool lean_nat_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
         // This comparison is UB according to the standard but allowed as per the
         // GCC documentation and the address sanitizer does not complain about it.
@@ -1299,7 +1307,7 @@ static inline bool lean_nat_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     }
 }
 
-static inline uint8_t lean_nat_dec_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
+static inline LEAN_ALWAYS_INLINE uint8_t lean_nat_dec_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     return lean_nat_lt(a1, a2);
 }
 
@@ -2691,7 +2699,7 @@ static inline size_t lean_float_to_usize(double a) {
     else
         return (size_t) lean_float_to_uint32(a); // NOLINT
 }
-LEAN_EXPORT double lean_float_from_bits(uint64_t u);
+LEAN_EXPORT double lean_float_of_bits(uint64_t u);
 LEAN_EXPORT uint64_t lean_float_to_bits(double d);
 static inline double lean_float_add(double a, double b) { return a + b; }
 static inline double lean_float_sub(double a, double b) { return a - b; }

src/runtime/object.cpp

@@ -1620,17 +1620,21 @@ extern "C" LEAN_EXPORT obj_res lean_float_frexp(double a) {
     return r;
 }
 
-extern "C" LEAN_EXPORT double lean_float_from_bits(uint64_t u)
+extern "C" LEAN_EXPORT double lean_float_of_bits(uint64_t u)
 {
     static_assert(sizeof(double) == sizeof(u), "`double` unexpected size.");
     double ret;
     std::memcpy(&ret, &u, sizeof(double));
+    if (isnan(ret))
+        ret = std::numeric_limits<double>::quiet_NaN();
     return ret;
 }
 
 extern "C" LEAN_EXPORT uint64_t lean_float_to_bits(double d)
 {
     uint64_t ret;
+    if (isnan(d))
+        d = std::numeric_limits<double>::quiet_NaN();
     std::memcpy(&ret, &d, sizeof(double));
     return ret;
 }

src/runtime/process.cpp

@@ -27,6 +27,10 @@ Author: Jared Roesch
 #include <limits.h> // NOLINT
 #endif
 
+#ifdef __linux
+#include <sys/syscall.h>
+#endif
+
 #include "runtime/object.h"
 #include "runtime/io.h"
 #include "runtime/array_ref.h"
@@ -80,6 +84,10 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_get_pid(obj_arg) {
     return lean_io_result_mk_ok(box_uint32(GetCurrentProcessId()));
 }
 
+extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg) {
+    return lean_io_result_mk_ok(box_uint64(GetCurrentThreadId()));
+}
+
 extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child, obj_arg) {
     HANDLE h = static_cast<HANDLE>(lean_get_external_data(cnstr_get(child, 3)));
     DWORD exit_code;
@@ -316,6 +324,20 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_get_pid(obj_arg) {
     return lean_io_result_mk_ok(box_uint32(getpid()));
 }
 
+extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg) {
+    uint64_t tid;
+#ifdef __APPLE__
+    lean_always_assert(pthread_threadid_np(NULL, &tid) == 0);
+#elif defined(LEAN_EMSCRIPTEN)
+    tid = 0;
+#else
+    // since Linux 2.4.11, our glibc 2.27 requires at least 3.2
+    // glibc 2.30 would provide a wrapper
+    tid = (pid_t)syscall(SYS_gettid);
+#endif
+    return lean_io_result_mk_ok(box_uint64(tid));
+}
+
 extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child, obj_arg) {
     static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT
     pid_t pid = cnstr_get_uint32(child, 3 * sizeof(object *));

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -56,8 +56,8 @@ a : α
           • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
             • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
           • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • FVarAlias a: _uniq.585 -> _uniq.312
-          • FVarAlias α: _uniq.584 -> _uniq.310
+          • FVarAlias a: _uniq.588 -> _uniq.315
+          • FVarAlias α: _uniq.587 -> _uniq.313
           • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
           • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
           • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -71,8 +71,8 @@ a : α
           • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
             • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
           • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • FVarAlias a: _uniq.616 -> _uniq.312
-          • FVarAlias n: _uniq.615 -> _uniq.310
+          • FVarAlias a: _uniq.619 -> _uniq.315
+          • FVarAlias n: _uniq.618 -> _uniq.313
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
             • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
             • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩

tests/lean/letFun.lean

@@ -55,10 +55,10 @@ Exercise `isDefEqQuick` for `let_fun`.
 Check that `let_fun` responds to WHNF's `zeta` option.
 -/
 
-open Lean Elab Term in
+open Lean Meta Elab Term in
 elab "#whnfCore " z?:(&"noZeta")? t:term : command => Command.runTermElabM fun _ => do
   let e ← withSynthesize <| Term.elabTerm t none
-  let e ← Meta.whnfCore e {zeta := z?.isNone}
+  let e ← withConfig (fun c => { c with zeta := z?.isNone }) <| Meta.whnfCore e
   logInfo m!"{e}"
 
 #whnfCore let_fun n := 5; n

tests/lean/run/3150.lean

@@ -0,0 +1,24 @@
+class One (α : Type) where
+  one : α
+
+variable (R A : Type) [One R] [One A]
+
+class OneHom where
+  toFun : R → A
+  map_one : toFun One.one = One.one
+
+structure Subone where
+  mem : R → Prop
+  one_mem : mem One.one
+
+structure Subalgebra [OneHom R A] extends Subone A : Type where
+  algebraMap_mem : ∀ r : R, mem (OneHom.toFun r)
+  one_mem := OneHom.map_one (R := R) (A := A) ▸ algebraMap_mem One.one
+
+/--
+error: fields missing: 'one_mem'
+-/
+#guard_msgs in
+example [OneHom R A] : Subalgebra R A where
+  mem := _
+  algebraMap_mem := _

tests/lean/run/ack.lean

@@ -5,14 +5,16 @@ def ack : Nat → Nat → Nat
 termination_by a b => (a, b)
 
 /--
-info: [reduction] unfolded declarations (max: 1725, num: 4):
-  [reduction] Nat.rec ↦ 1725
-  [reduction] Eq.rec ↦ 1114
-  [reduction] Acc.rec ↦ 1050
-  [reduction] PSigma.rec ↦ 513[reduction] unfolded reducible declarations (max: 1577, num: 3):
-  [reduction] Nat.casesOn ↦ 1577
-  [reduction] Eq.ndrec ↦ 984
-  [reduction] PSigma.casesOn ↦ 513[kernel] unfolded declarations (max: 1193, num: 5):
+info: [reduction] unfolded declarations (max: 2567, num: 5):
+  [reduction] Nat.rec ↦ 2567
+  [reduction] Eq.rec ↦ 1517
+  [reduction] Acc.rec ↦ 1158
+  [reduction] Or.rec ↦ 770
+  [reduction] PSigma.rec ↦ 514[reduction] unfolded reducible declarations (max: 2337, num: 4):
+  [reduction] Nat.casesOn ↦ 2337
+  [reduction] Eq.ndrec ↦ 1307
+  [reduction] Or.casesOn ↦ 770
+  [reduction] PSigma.casesOn ↦ 514[kernel] unfolded declarations (max: 1193, num: 5):
   [kernel] Nat.casesOn ↦ 1193
   [kernel] Nat.rec ↦ 1065
   [kernel] Eq.ndrec ↦ 973

tests/lean/run/atomValidation.lean

@@ -0,0 +1,138 @@
+import Lean.Elab.Command
+import Lean.Elab.Syntax
+
+open Lean.Elab.Term.toParserDescr (isValidAtom)
+open Lean Elab Command
+
+/-!
+Test various classes of atoms that should be allowed or not.
+-/
+
+def test (expected : Bool) (strings : List String) : CommandElabM Unit := Id.run do
+  let mut wrong : List String := []
+  for s in strings do
+    if isValidAtom s != expected then
+      wrong := s :: wrong
+    if isValidAtom (" " ++ s) != expected then
+      wrong := s!"{s} (with leading whitespace)" :: wrong
+    if isValidAtom (s ++ " ") != expected then
+      wrong := s!"{s} (with trailing whitespace)" :: wrong
+    if isValidAtom (" " ++ s ++ " ") != expected then
+      wrong := s!"{s} (with leading and trailing whitespace)" :: wrong
+
+  if wrong.isEmpty then
+    logInfo <| "All " ++ if expected then "accepted" else "rejected"
+  else
+    logError <|
+      s!"The following atoms should be {if expected then "" else "in"}valid but are not:\n" ++
+      String.join (wrong.reverse.map (s! " * {·}\n"))
+
+
+syntax "#test_valid" term : command
+syntax "#test_invalid" term : command
+
+macro_rules
+  | `(#test_valid%$tok $t) => `(#eval%$tok test true $t)
+  | `(#test_invalid%$tok $t) => `(#eval%$tok test false $t)
+
+
+/-!
+# No Empty Atoms
+-/
+
+/-- info: All rejected -/
+#guard_msgs in
+#test_invalid [""]
+
+
+/-!
+# Preventing Character Literal Confusion
+
+Atoms are required to be suitably unlike character literals. This means that if they start with a
+single quote, the next character must also be a single quote.
+
+Two single quotes (and variations on it) has long-term usage as an infix operator in Mathlib.
+-/
+
+/-- info: All accepted -/
+#guard_msgs in
+#test_valid ["if", "''", "''ᵁ", "if'", "x'y'z", "x''y"]
+
+/-- info: All rejected -/
+#guard_msgs in
+#test_invalid ["'x'", "'ᵁ", "'c", "'no'", "'"]
+
+
+/-!
+# No Internal Whitespace
+-/
+
+/-- info: All rejected -/
+#guard_msgs in
+#test_invalid ["open mixed", "open   mixed"]
+
+
+/-!
+# No Confusion with String Literals
+
+Internal double quotes are allowed.
+-/
+
+/-- info: All accepted -/
+#guard_msgs in
+#test_valid ["what\"string\"is_this?"]
+
+/-- info: All rejected -/
+#guard_msgs in
+#test_invalid ["\"","\"\"", "\"f\""]
+
+/-!
+# No Confusion with Escaped Identifiers
+
+This doesn't confuse the parser, but it may confuse a user if they can define an atom that can never
+be parsed.
+-/
+
+/-- info: All accepted -/
+#guard_msgs in
+#test_valid ["prefix«", "prefix«test", "prefix«test»", "prefix«test»foo"]
+
+/-- info: All rejected -/
+#guard_msgs in
+#test_invalid ["«", "«test", "«test»", "«test»foo"]
+
+
+/-!
+# No Confusion with Name Literals
+
+The first two characters of an atom may not be a valid start of a name literal
+-/
+
+/-- info: All accepted -/
+#guard_msgs in
+#test_valid ["``", "`!", "x`"]
+
+/-!
+The next set all begin with U0x2035, REVERSED PRIME, rather than back-tick, and are thus accepted.
+-/
+/-- info: All accepted -/
+#guard_msgs in
+#test_valid ["‵", "‵x", "‵«", "‵xyz", "‵«x.y", "‵«x.y.z»"]
+
+
+/-- info: All rejected -/
+#guard_msgs in
+#test_invalid ["`", "`x", "`«", "`xyz", "`«x.y", "`«x.y.z»"]
+
+
+/-!
+# No Leading Digits
+-/
+
+/-- info: All accepted -/
+#guard_msgs in
+#test_valid ["prefix5", "prefix22test", "prefix1test0", "prefix8test8foo"]
+
+/-- info: All rejected -/
+#guard_msgs in
+#test_invalid ["0", "1test", "0test3"]

tests/lean/run/canonM_exists_fun.lean

@@ -0,0 +1,22 @@
+import Lean.Meta.Canonicalizer
+import Lean.Elab.Tactic
+
+elab "foo" t:term : tactic => do
+  let e ← Lean.Elab.Tactic.elabTerm t none
+  trace[debug] "canonicalizing {e}"
+  let e' ← (Lean.Meta.canon e).run'
+  trace[debug] "canonicalized it to {e'}"
+
+/-- info: ∃ f, ∀ (x : Nat), f x = 0 : Prop -/
+#guard_msgs in
+#check (∃ f : Nat → Nat, ∀ x, f x = 0) -- works fine
+
+/--
+info: [debug] canonicalizing ∃ f, ∀ (x : Nat), f x = 0
+[debug] canonicalized it to ∃ f, ∀ (x : Nat), f x = 0
+-/
+#guard_msgs in
+set_option trace.debug true in
+example : True := by
+  foo (∃ f : Nat → Nat, ∀ x, f x = 0) -- used to fail with "unexpected bound variable #1"
+  trivial

tests/lean/run/change.lean

@@ -2,7 +2,7 @@
 private axiom test_sorry : ∀ {α}, α
 
 set_option linter.missingDocs false
-set_option autoImplicit true
+set_option pp.mvars false
 
 example : n + 2 = m := by
   change n + 1 + 1 = _
@@ -40,6 +40,10 @@ noncomputable example : Nat := by
 
 def foo (a b c : Nat) := if a < b then c else 0
 
+/-!
+The first `change` would fail with `typeclass instance problem is stuck` if we did not have
+the `Term.synthesizeSyntheticMVars (postpone := .partial); discard <| isDefEq p e` hint
+-/
 example : foo 1 2 3 = 3 := by
   change (if _ then _ else _) = _
   change ite _ _ _ = _
@@ -65,16 +69,143 @@ example (α : Type) [LT α] (x : α) (h : x < x) : x < id x := by
   guard_target =ₛ x < x
   exact h
 
--- This example shows using named and anonymous placeholders to create a new goal.
+/-!
+basic failure
+-/
+/--
+error: 'change' tactic failed, pattern
+  m = ?_
+is not definitionally equal to target
+  n = m
+-/
+#guard_msgs in example : n = m := by
+  change m = _
+
+/-!
+`change` can create new metavariables and assign them
+-/
+/--
+info: x y z : Nat
+w : Nat := x + y
+⊢ x + y = z
+-/
+#guard_msgs in
+example (x y z : Nat) : x + y = z := by
+  change ?a = _
+  let w := ?a
+  trace_state
+  exact test_sorry
+
+/-!
+`change` is allowed to create new goals.
+Motivation: sometimes there are proof arguments that need to be filled in, and it is easier to do so as a new goal.
+-/
 example (x y : Nat) (h : x = y) : True := by
-  change (if 1 < 2 then x else ?z + ?_) = y at h
-  rotate_left
-  · exact 4
-  · exact 37
-  guard_hyp h : (if 1 < 2 then x else 4 + 37) = y
+  change (if 1 < 2 then x else ?z) = y at h
   · trivial
+  · exact 22
 
 example : let x := 22; let y : Nat := x; let z : Fin (y + 1) := 0; z.1 < y + 1 := by
   intro x y z -- `z` was previously erroneously marked as unused
   change _ at y
   exact z.2
+
+/-!
+`change` reorders hypotheses if necessary
+-/
+/--
+info: x y z w : Nat
+a : Nat := x + y
+h : a = z + w
+⊢ True
+-/
+#guard_msgs in
+example (x y z w : Nat) (h : x + y = z + w) : True := by
+  let a := x + y
+  change a = _ at h
+  trace_state
+  trivial
+
+/-!
+`change` inserts a coercion when types are incompatible.
+-/
+example (ty : {α : Prop // Nonempty α}) : ty.val := by
+  change ty
+  guard_target =ₛ ty.val
+  exact test_sorry
+
+/-!
+Fails, type hint can't hint enough since `.some _` is postponed.
+-/
+/--
+error: invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
+  ?_
+-/
+#guard_msgs in example : some true = (some true).map id := by
+  change _ = .some _
+
+/-!
+That works with a mild type hint.
+-/
+example : some true = (some true).map id := by
+  change _ = (.some _ : Option _)
+  rfl
+
+
+/-!
+## Conv `change`
+-/
+
+/-!
+conv `change` test
+-/
+example (m n : Nat) : m + 2 = n := by
+  conv => enter [1]; change m + (1 + 1)
+  guard_target =ₛ m + (1 + 1) = n
+  exact test_sorry
+
+/-!
+conv `change` test failure
+-/
+/--
+error: 'change' tactic failed, pattern
+  m + n
+is not definitionally equal to target
+  m + 2
+-/
+#guard_msgs in
+example (m n : Nat) : m + 2 = n := by
+  conv => enter [1]; change m + n
+
+/-!
+conv `change` unsolved metavariables
+-/
+/--
+error: don't know how to synthesize placeholder for argument 'e'
+context:
+case a
+m n : Nat
+⊢ Nat
+---
+error: unsolved goals
+m n : Nat
+⊢ m + 2 = n
+-/
+#guard_msgs in
+example (m n : Nat) : m + 2 = n := by
+  conv => enter [1]; change if True then m + 2 else ?a
+
+/-!
+conv `change` to create a metavariable
+-/
+/--
+info: a b c d : Nat
+e : Nat := a + b
+⊢ a + b + c = d
+-/
+#guard_msgs in
+example (a b c d : Nat) : a + b + c = d := by
+  conv => enter [1,1]; change ?mvar
+  let e := ?mvar
+  trace_state
+  exact test_sorry

tests/lean/run/change_tac.lean

@@ -1,76 +0,0 @@
-private axiom test_sorry : ∀ {α}, α
-
-example : n + 2 = m := by
-  change n + 1 + 1 = _
-  guard_target =ₛ n + 1 + 1 = m
-  exact test_sorry
-
-example (h : n + 2 = m) : False := by
-  change _ + 1 = _ at h
-  guard_hyp h :ₛ n + 1 + 1 = m
-  exact test_sorry
-
-example : n + 2 = m := by
-  fail_if_success change true
-  fail_if_success change _ + 3 = _
-  fail_if_success change _ * _ = _
-  change (_ : Nat) + _ = _
-  exact test_sorry
-
--- `change ... at ...` allows placeholders to mean different things at different hypotheses
-example (h : n + 3 = m) (h' : n + 2 = m) : False := by
-  change _ + 1 = _ at h h'
-  guard_hyp h :ₛ n + 2 + 1 = m
-  guard_hyp h' :ₛ n + 1 + 1 = m
-  exact test_sorry
-
--- `change ... at ...` preserves dependencies
-example (p : n + 2 = m → Type) (h : n + 2 = m) (x : p h) : false := by
-  change _ + 1 = _ at h
-  guard_hyp x :ₛ p h
-  exact test_sorry
-
-noncomputable example : Nat := by
-  fail_if_success change Type 1
-  exact test_sorry
-
-def foo (a b c : Nat) := if a < b then c else 0
-
-example : foo 1 2 3 = 3 := by
-  change (if _ then _ else _) = _
-  change ite _ _ _ = _
-  change (if _ < _ then _ else _) = _
-  change _ = (if true then 3 else 4)
-  rfl
-
-example (h : foo 1 2 3 = 4) : True := by
-  change ite _ _ _ = _ at h
-  guard_hyp h :ₛ ite (1 < 2) 3 0 = 4
-  trivial
-
-example (h : foo 1 2 3 = 4) : True := by
-  change (if _ then _ else _) = _ at h
-  guard_hyp h : (if 1 < 2 then 3 else 0) = 4
-  trivial
-
-example (α : Type) [LT α] (x : α) (h : x < x) : x < id x := by
-  change _ < _ -- can defer LT typeclass lookup, just like `show`
-  change _ < _ at h -- can defer LT typeclass lookup at h too
-  guard_target =ₛ x < id x
-  change _ < x
-  guard_target =ₛ x < x
-  exact h
-
--- This example shows using named and anonymous placeholders to create a new goal.
-example (x y : Nat) (h : x = y) : True := by
-  change (if 1 < 2 then x else ?z + ?_) = y at h
-  rotate_left
-  · exact 4
-  · exact 37
-  guard_hyp h : (if 1 < 2 then x else 4 + 37) = y
-  · trivial
-
-example : let x := 22; let y : Nat := x; let z : Fin (y + 1) := 0; z.1 < y + 1 := by
-  intro x y z -- `z` was previously erroneously marked as unused
-  change _ at y
-  exact z.2

tests/lean/run/decideTacticKernel.lean

@@ -1,12 +1,12 @@
 /-!
-# `decide!` tests
+# `decide +kernel` tests
 -/
 
 /-!
 Very basic tests
 -/
 theorem foo1 : True := by decide
-theorem foo2 : True := by decide!
+theorem foo2 : True := by decide +kernel
 
 /-!
 Tests of the error message when goal is false.
@@ -21,12 +21,12 @@ is false
 theorem foo3 : False := by decide
 
 /--
-error: tactic 'decide!' proved that the proposition
+error: tactic 'decide' proved that the proposition
   False
 is false
 -/
 #guard_msgs in
-theorem foo4 : False := by decide!
+theorem foo4 : False := by decide +kernel
 
 /-!
 The kernel sees through irreducible definitions
@@ -47,26 +47,26 @@ After unfolding the instances 'instDecidableEqNat' and 'Nat.decEq', reduction go
 -/
 #guard_msgs in theorem gcd_eq1 : irred 3 = 3 := by decide
 
-theorem gcd_eq2 : irred 3 = 3 := by decide!
+theorem gcd_eq2 : irred 3 = 3 := by decide +kernel
 
 
 /-!
-The proofs from `decide!` are cached.
+The proofs from `decide +kernel` are cached.
 -/
 
-theorem thm1 : ∀ x < 100, x * x ≤ 10000 := by decide!
+theorem thm1 : ∀ x < 100, x * x ≤ 10000 := by decide +kernel
 
-theorem thm1' : ∀ x < 100, x * x ≤ 10000 := by decide!
+theorem thm1' : ∀ x < 100, x * x ≤ 10000 := by decide +kernel
 
 -- (Note: when run within VS Code, these tests fail since the auxLemmas have a `lean.run` prefix.)
 /--
 info: theorem thm1 : ∀ (x : Nat), x < 100 → x * x ≤ 10000 :=
-decideBang._auxLemma.3
+decideTacticKernel._auxLemma.3
 -/
 #guard_msgs in #print thm1
 /--
 info: theorem thm1' : ∀ (x : Nat), x < 100 → x * x ≤ 10000 :=
-decideBang._auxLemma.3
+decideTacticKernel._auxLemma.3
 -/
 #guard_msgs in #print thm1'
 
@@ -81,9 +81,9 @@ error: expected type must not contain free variables
 Use the '+revert' option to automatically cleanup and revert free variables.
 -/
 #guard_msgs in
-example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide!
+example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide +kernel
 
-example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide! +revert
+example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide +kernel +revert
 
 
 /--
@@ -93,4 +93,4 @@ Can handle universe levels.
 instance (p : PUnit.{u} → Prop) [Decidable (p PUnit.unit)] : Decidable (∀ x : PUnit.{u}, p x) :=
   decidable_of_iff (p PUnit.unit) (by constructor; rintro _ ⟨⟩; assumption; intro h; apply h)
 
-example : ∀ (x : PUnit.{u}), x = PUnit.unit := by decide!
+example : ∀ (x : PUnit.{u}), x = PUnit.unit := by decide +kernel

tests/lean/run/floatBits.lean

@@ -10,4 +10,40 @@ info: 4608285800708723180
 info: true
 -/
 #guard_msgs in
-#eval Float.fromBits d.toBits == d
+#eval Float.ofBits d.toBits == d
+
+/--
+info: NaN
+-/
+#guard_msgs in
+#eval Float.ofBits 9221120237041090560
+/--
+info: NaN
+-/
+#guard_msgs in
+#eval Float.ofBits 18444492273895866368
+
+/--
+info: 9221120237041090560
+-/
+#guard_msgs in
+#eval (Float.ofBits 9221120237041090560).toBits
+
+/--
+info: 9221120237041090560
+-/
+#guard_msgs in
+#eval (Float.ofBits 18444492273895866368).toBits
+
+/--
+info: 9221120237041090560
+-/
+#guard_msgs in
+#eval (1.0/0.0 - 1.0/0.0).toBits
+
+/--
+info: 9221120237041090560
+-/
+-- Should also produce quiet_NaN
+#guard_msgs in
+#eval (-(1.0/0.0 - 1.0/0.0)).toBits

tests/lean/run/funind_tests.lean

@@ -573,7 +573,7 @@ end RecCallInDisrs
 namespace EvenOdd
 
 mutual
-def even : Nat → Bool
+def even : (m : Nat) → Bool -- NB: Does this parameter name appear in the inductions?
   | 0 => true
   | n+1 => odd n
 termination_by n => n
@@ -585,7 +585,7 @@ end
 
 /--
 info: EvenOdd.even.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ)
-  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) (a✝ : Nat) : motive1 a✝
+  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) (m : Nat) : motive1 m
 -/
 #guard_msgs in
 #check even.induct
@@ -597,6 +597,14 @@ info: EvenOdd.odd.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (c
 #guard_msgs in
 #check odd.induct
 
+/--
+info: EvenOdd.even.mutual_induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0)
+  (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ) (case3 : motive2 0)
+  (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : (∀ (m : Nat), motive1 m) ∧ ∀ (a : Nat), motive2 a
+-/
+#guard_msgs in
+#check even.mutual_induct
+
 end EvenOdd
 
 namespace Tree

tests/lean/run/issue6015.lean

@@ -0,0 +1,21 @@
+private axiom test_sorry : ∀ {α}, α
+
+inductive Tyₛ (l : List Unit): Type
+| U : Tyₛ l
+open Tyₛ
+
+inductive Varₚ (d : Unit): List Unit → Type
+| vz : Varₚ d [d']
+| vs : Varₚ d l → Varₚ d (Bₛ :: l)
+
+inductive Tmₛ {l : List Unit}: Tyₛ l → Unit → Type 1
+| arr   : (T : Type) → Tmₛ A d → Tmₛ A d
+| param : Varₚ d l → Tmₛ A d → Tmₛ (@U l) d
+
+def TmₛA {l : List Unit} {d : Unit} (nonIndex : Bool) {Aₛ : Tyₛ l} (t : Tmₛ Aₛ d): Type :=
+match t with
+  | .arr dom cd =>
+    let cd := TmₛA nonIndex cd
+    dom → cd
+  | _ => test_sorry
+termination_by structural t

tests/lean/run/meta3.lean

@@ -34,25 +34,25 @@ def add  := mkAppN (mkConst `Add.add [levelZero]) #[nat, mkConst `Nat.add]
 def tst1 : MetaM Unit :=
 do let d : DiscrTree Nat := {};
    let mvar ← mkFreshExprMVar nat;
-   let d ← d.insert (mkAppN add #[mvar, mkNatLit 10]) 1 {}
-   let d ← d.insert (mkAppN add #[mkNatLit 0, mkNatLit 10]) 2 {}
-   let d ← d.insert (mkAppN (mkConst `Nat.add) #[mkNatLit 0, mkNatLit 20]) 3 {}
-   let d ← d.insert (mkAppN add #[mvar, mkNatLit 20]) 4 {}
-   let d ← d.insert mvar 5 {}
+   let d ← d.insert (mkAppN add #[mvar, mkNatLit 10]) 1
+   let d ← d.insert (mkAppN add #[mkNatLit 0, mkNatLit 10]) 2
+   let d ← d.insert (mkAppN (mkConst `Nat.add) #[mkNatLit 0, mkNatLit 20]) 3
+   let d ← d.insert (mkAppN add #[mvar, mkNatLit 20]) 4
+   let d ← d.insert mvar 5
    print (format d);
-   let vs ← d.getMatch (mkAppN add #[mkNatLit 1, mkNatLit 10]) {};
+   let vs ← d.getMatch (mkAppN add #[mkNatLit 1, mkNatLit 10]);
    print (format vs);
    let t := mkAppN add #[mvar, mvar];
    print t;
-   let vs ← d.getMatch t {};
+   let vs ← d.getMatch t
    print (format vs);
-   let vs ← d.getUnify t {};
+   let vs ← d.getUnify t;
    print (format vs);
-   let vs ← d.getUnify mvar {};
+   let vs ← d.getUnify mvar;
    print (format vs);
-   let vs ← d.getUnify (mkAppN add #[mkNatLit 0, mvar]) {};
+   let vs ← d.getUnify (mkAppN add #[mkNatLit 0, mvar]);
    print (format vs);
-   let vs ← d.getUnify (mkAppN add #[mvar, mkNatLit 20]) {};
+   let vs ← d.getUnify (mkAppN add #[mvar, mkNatLit 20]);
    print (format vs);
    pure ()
 

tests/lean/run/meta5.lean

@@ -28,11 +28,11 @@ info: [Meta.debug] ?_
 [Meta.debug] fun y =>
       let x := 0;
       x.add y
-[Meta.debug] ?_uniq.3019 : Nat →
+[Meta.debug] ?_uniq.3037 : Nat
+[Meta.debug] ?_uniq.3038 : Nat →
       Nat →
         let x := 0;
         Nat
-[Meta.debug] ?_uniq.3018 : Nat
 -/
 #guard_msgs in
 #eval tst1

tests/lean/run/ppParens.lean

@@ -0,0 +1,56 @@
+/-!
+# Tests for the `pp.parens` pretty printing option
+-/
+
+set_option pp.parens true
+
+/-!
+No parentheses around numeral.
+-/
+/-- info: 1 : Nat -/
+#guard_msgs in #check 1
+
+/-!
+No parentheses around variable.
+-/
+/-- info: x : Nat -/
+#guard_msgs in variable (x : Nat) in #check x
+
+/-!
+No parentheses around each individual function application.
+-/
+def f (x y z : Nat) : Nat := x + y + z
+/-- info: f 1 2 3 : Nat -/
+#guard_msgs in #check f 1 2 3
+
+/-!
+Example arithmetic expressions
+-/
+/-- info: (1 + (2 * 3)) + 4 : Nat -/
+#guard_msgs in #check 1 + 2 * 3 + 4
+/-- info: Nat.add_assoc : ∀ (n m k : Nat), (((n + m) + k) = (n + (m + k))) -/
+#guard_msgs in #check (Nat.add_assoc)
+
+/-!
+Implication chains
+-/
+/-- info: p → (q → r) : Prop -/
+#guard_msgs in variable (p q r : Prop) in #check p → q → r
+
+/-!
+No parentheses around list literals
+-/
+/-- info: [1, 2, 3] ++ [3, 4, 5] : List Nat -/
+#guard_msgs in #check [1,2,3] ++ [3,4,5]
+
+/-!
+Parentheses around body of forall.
+-/
+/-- info: ∀ (p : (Nat → (Nat → Prop))), (p (1 + 2) 3) : Prop -/
+#guard_msgs in #check ∀ (p : Nat → Nat → Prop), p (1 + 2) 3
+
+/-!
+Parentheses around branches of `if`.
+-/
+/-- info: if True then (1 + 2) else (2 + 3) : Nat -/
+#guard_msgs in #check if True then 1 + 2 else 2 + 3

tests/lean/run/simp1.lean

@@ -44,7 +44,7 @@ def tst2 : MetaM Unit := do
     | some (_, lhs, _) =>
       trace[Meta.debug] "lhs: {lhs}"
       let s ← Meta.getSimpTheorems
-      let m ← s.post.getMatch lhs {}
+      let m ← s.post.getMatch lhs
       trace[Meta.debug] "result: {m}"
       assert! m.any fun s => s.origin == .decl `ex2