chore: cleanup

This PR implements `PersistentHashMap.findKeyD` and
`PersistentHashSet.findD`. The motivation is avoid two memory
allocations (`Prod.mk` and `Option.some`) when the collections contains
the key.

.claude/CLAUDE.md

@@ -29,6 +29,19 @@ After rebuilding, LSP diagnostics may be stale until the user interacts with fil
 
 If the user expresses frustration with you, stop and ask them to help update this `.claude/CLAUDE.md` file with missing guidance.
 
-## Creating pull requests.
+## Creating pull requests
 
-All PRs must have a first paragraph starting with "This PR". This paragraph is automatically incorporated into release notes. Read `lean4/doc/dev/commit_convention.md` when making PRs.
+Follow the commit convention in `doc/dev/commit_convention.md`.
+
+**Title format:** `<type>: <subject>` where type is one of: `feat`, `fix`, `doc`, `style`, `refactor`, `test`, `chore`, `perf`.
+Subject should use imperative present tense ("add" not "added"), no capitalization, no trailing period.
+
+**Body format:** The first paragraph must start with "This PR". This paragraph is automatically incorporated into release notes. Use imperative present tense. Include motivation and contrast with previous behavior when relevant.
+
+Example:
+```
+feat: add optional binder limit to `mkPatternFromTheorem`
+
+This PR adds a `num?` parameter to `mkPatternFromTheorem` to control how many
+leading quantifiers are stripped when creating a pattern.
+```

script/release_repos.yml

@@ -142,3 +142,15 @@ repositories:
     branch: master
     dependencies:
       - verso-web-components
+
+  - name: comparator
+    url: https://github.com/leanprover/comparator
+    toolchain-tag: true
+    stable-branch: false
+    branch: master
+
+  - name: lean4export
+    url: https://github.com/leanprover/lean4export
+    toolchain-tag: true
+    stable-branch: false
+    branch: master

src/Init/Data/Array/Lemmas.lean

@@ -115,7 +115,8 @@ theorem none_eq_getElem?_iff {xs : Array α} {i : Nat} : none = xs[i]? ↔ xs.si
 theorem getElem?_eq_none {xs : Array α} (h : xs.size ≤ i) : xs[i]? = none := by
   simp [h]
 
-grind_pattern Array.getElem?_eq_none => xs.size, xs[i]?
+grind_pattern Array.getElem?_eq_none => xs.size, xs[i]? where
+  guard xs.size ≤ i
 
 @[simp] theorem getElem?_eq_getElem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i]? = some xs[i] :=
   getElem?_pos ..

src/Init/Data/BitVec/Lemmas.lean

@@ -67,6 +67,9 @@ theorem none_eq_getElem?_iff {l : BitVec w} : none = l[n]? ↔ w ≤ n := by
 @[simp]
 theorem getElem?_eq_none {l : BitVec w} (h : w ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
 
+grind_pattern BitVec.getElem?_eq_none => l[n]? where
+  guard w ≤ n
+
 theorem getElem?_eq (l : BitVec w) (i : Nat) :
     l[i]? = if h : i < w then some l[i] else none := by
   split <;> simp_all

src/Init/Data/Int/Gcd.lean

@@ -113,6 +113,8 @@ theorem gcd_eq_right_iff_dvd (hb : 0 ≤ b) : gcd a b = b ↔ b ∣ a := by
 
 theorem gcd_assoc (a b c : Int) : gcd (gcd a b) c = gcd a (gcd b c) := Nat.gcd_assoc ..
 
+theorem gcd_left_comm (a b c : Int) : gcd a (gcd b c) = gcd b (gcd a c) := Nat.gcd_left_comm ..
+
 theorem gcd_mul_left (m n k : Int) : gcd (m * n) (m * k) = m.natAbs * gcd n k := by
   simp [gcd_eq_natAbs_gcd_natAbs, Nat.gcd_mul_left, natAbs_mul]
 

src/Init/Data/Iterators/Basic.lean

@@ -932,4 +932,60 @@ class LawfulDeterministicIterator (α : Type w) (m : Type w → Type w') [Iterat
     where
   isPlausibleStep_eq_eq : ∀ it : IterM (α := α) m β, ∃ step, it.IsPlausibleStep = (· = step)
 
-end Std
+namespace Iterators
+
+/--
+This structure provides a more convenient way to define `Finite α m` instances using
+`Finite.of_finitenessRelation : FinitenessRelation α m → Finite α m`.
+-/
+structure FinitenessRelation (α : Type w) (m : Type w → Type w') {β : Type w}
+    [Iterator α m β] where
+  /-
+  A well-founded relation such that if `it'` is a successor iterator of `it`, then
+  `Rel it' it`.
+  -/
+  Rel (it' it : IterM (α := α) m β) : Prop
+  /- A proof that `Rel` is well-founded. -/
+  wf : WellFounded Rel
+  /- A proof that if `it'` is a successor iterator of `it`, then `Rel it' it`. -/
+  subrelation : ∀ {it it'}, it'.IsPlausibleSuccessorOf it → Rel it' it
+
+theorem Finite.of_finitenessRelation
+    {α : Type w} {m : Type w → Type w'} {β : Type w}
+    [Iterator α m β] (r : FinitenessRelation α m) : Finite α m where
+  wf := by
+    refine Subrelation.wf (r := r.Rel) ?_ ?_
+    · intro x y h
+      apply FinitenessRelation.subrelation
+      exact h
+    · apply InvImage.wf
+      exact r.wf
+
+/--
+This structure provides a more convenient way to define `Productive α m` instances using
+`Productive.of_productivenessRelation : ProductivenessRelation α m → Productive α m`.
+-/
+structure ProductivenessRelation (α : Type w) (m : Type w → Type w') {β : Type w}
+    [Iterator α m β] where
+  /-
+  A well-founded relation such that if `it'` is obtained from `it` by skipping, then
+  `Rel it' it`.
+  -/
+  Rel : (IterM (α := α) m β) → (IterM (α := α) m β) → Prop
+  /- A proof that `Rel` is well-founded. -/
+  wf : WellFounded Rel
+  /- A proof that if `it'` is obtained from `it` by skipping, then `Rel it' it`. -/
+  subrelation : ∀ {it it'}, it'.IsPlausibleSkipSuccessorOf it → Rel it' it
+
+theorem Productive.of_productivenessRelation
+    {α : Type w} {m : Type w → Type w'} {β : Type w}
+    [Iterator α m β] (r : ProductivenessRelation α m) : Productive α m where
+  wf := by
+    refine Subrelation.wf (r := r.Rel) ?_ ?_
+    · intro x y h
+      apply ProductivenessRelation.subrelation
+      exact h
+    · apply InvImage.wf
+      exact r.wf
+
+end Std.Iterators

src/Init/Data/Iterators/Combinators/Monadic/Attach.lean

@@ -6,7 +6,6 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Data.Iterators.Internal.Termination
 public import Init.Data.Iterators.Consumers.Loop
 
 public section
@@ -47,7 +46,7 @@ instance Attach.instIterator {α β : Type w} {m : Type w → Type w'} [Monad m]
 def Attach.instFinitenessRelation {α β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α m β] [Finite α m] {P : β → Prop} :
     FinitenessRelation (Attach α m P) m where
-  rel := InvImage WellFoundedRelation.rel fun it => it.internalState.inner.finitelyManySteps
+  Rel := InvImage WellFoundedRelation.rel fun it => it.internalState.inner.finitelyManySteps
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     apply Relation.TransGen.single
@@ -68,7 +67,7 @@ instance Attach.instFinite {α β : Type w} {m : Type w → Type w'} [Monad m]
 def Attach.instProductivenessRelation {α β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α m β] [Productive α m] {P : β → Prop} :
     ProductivenessRelation (Attach α m P) m where
-  rel := InvImage WellFoundedRelation.rel fun it => it.internalState.inner.finitelyManySkips
+  Rel := InvImage WellFoundedRelation.rel fun it => it.internalState.inner.finitelyManySkips
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     apply Relation.TransGen.single

src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.PostconditionMonad
-public import Init.Data.Iterators.Internal.Termination
 
 public section
 
@@ -172,7 +171,7 @@ private def FilterMap.instFinitenessRelation {α β γ : Type w} {m : Type w →
     {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n (Option γ)} [Finite α m] :
     FinitenessRelation (FilterMap α m n lift f) n where
-  rel := InvImage IterM.IsPlausibleSuccessorOf (FilterMap.inner ∘ IterM.internalState)
+  Rel := InvImage IterM.IsPlausibleSuccessorOf (FilterMap.inner ∘ IterM.internalState)
   wf := InvImage.wf _ Finite.wf
   subrelation {it it'} h := by
     obtain ⟨step, h, h'⟩ := h
@@ -205,7 +204,7 @@ private def Map.instProductivenessRelation {α β γ : Type w} {m : Type w → T
     {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n γ} [Productive α m] :
     ProductivenessRelation (Map α m n lift f) n where
-  rel := InvImage IterM.IsPlausibleSkipSuccessorOf (FilterMap.inner ∘ IterM.internalState)
+  Rel := InvImage IterM.IsPlausibleSkipSuccessorOf (FilterMap.inner ∘ IterM.internalState)
   wf := InvImage.wf _ Productive.wf
   subrelation {it it'} h := by
     cases h

src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean

@@ -277,7 +277,7 @@ theorem Flatten.rel_of_right₂ [Monad m] [Iterator α m (IterM (α := α₂) m
 def Flatten.instFinitenessRelation [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
     [Finite α m] [Finite α₂ m] :
     FinitenessRelation (Flatten α α₂ β m) m where
-  rel := Rel α β m
+  Rel := Rel α β m
   wf := by
     apply InvImage.wf
     refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
@@ -342,7 +342,7 @@ theorem Flatten.productiveRel_of_right₂ [Monad m] [Iterator α m (IterM (α :=
 def Flatten.instProductivenessRelation [Monad m] [Iterator α m (IterM (α := α₂) m β)]
     [Iterator α₂ m β] [Finite α m] [Productive α₂ m] :
     ProductivenessRelation (Flatten α α₂ β m) m where
-  rel := ProductiveRel α β m
+  Rel := ProductiveRel α β m
   wf := by
     apply InvImage.wf
     refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩

src/Init/Data/Iterators/Combinators/Monadic/Take.lean

@@ -9,7 +9,6 @@ prelude
 public import Init.Data.Nat.Lemmas
 public import Init.Data.Iterators.Consumers.Monadic.Collect
 public import Init.Data.Iterators.Consumers.Monadic.Loop
-public import Init.Data.Iterators.Internal.Termination
 
 @[expose] public section
 
@@ -165,7 +164,7 @@ theorem Take.rel_of_zero_of_inner [Monad m] [Iterator α m β]
 private def Take.instFinitenessRelation [Monad m] [Iterator α m β]
     [Productive α m] :
     FinitenessRelation (Take α m) m where
-  rel := Take.Rel m
+  Rel := Take.Rel m
   wf := by
     rw [Rel]
     split

src/Init/Data/Iterators/Combinators/Monadic/ULift.lean

@@ -6,7 +6,6 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Data.Iterators.Internal.Termination
 public import Init.Data.Iterators.Consumers.Monadic
 
 public section
@@ -99,7 +98,7 @@ instance ULiftIterator.instIterator [Iterator α m β] [Monad n] :
 
 private def ULiftIterator.instFinitenessRelation [Iterator α m β] [Finite α m] [Monad n] :
     FinitenessRelation (ULiftIterator α m n β lift) n where
-  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.inner.finitelyManySteps)
+  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.inner.finitelyManySteps)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation h := by
     rcases h with ⟨_, hs, step, hp, rfl⟩
@@ -115,7 +114,7 @@ instance ULiftIterator.instFinite [Iterator α m β] [Finite α m] [Monad n] :
 
 private def ULiftIterator.instProductivenessRelation [Iterator α m β] [Productive α m] [Monad n] :
     ProductivenessRelation (ULiftIterator α m n β lift) n where
-  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.inner.finitelyManySkips)
+  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.inner.finitelyManySkips)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation h := by
     rcases h with ⟨step, hp, hs⟩

src/Init/Data/Iterators/Internal.lean

@@ -7,4 +7,3 @@ module
 
 prelude
 public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
-public import Init.Data.Iterators.Internal.Termination

src/Init/Data/Iterators/Internal/Termination.lean

@@ -1,63 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.Iterators.Basic
-
-public section
-
-/-!
-This is an internal module used by iterator implementations.
--/
-
-namespace Std.Iterators
-
-/--
-Internal implementation detail of the iterator library.
-The purpose of this class is that it implies a `Finite` instance but
-it is more convenient to implement.
--/
-structure FinitenessRelation (α : Type w) (m : Type w → Type w') {β : Type w}
-    [Iterator α m β] where
-  rel : (IterM (α := α) m β) → (IterM (α := α) m β) → Prop
-  wf : WellFounded rel
-  subrelation : ∀ {it it'}, it'.IsPlausibleSuccessorOf it → rel it' it
-
-theorem Finite.of_finitenessRelation
-    {α : Type w} {m : Type w → Type w'} {β : Type w}
-    [Iterator α m β] (r : FinitenessRelation α m) : Finite α m where
-  wf := by
-    refine Subrelation.wf (r := r.rel) ?_ ?_
-    · intro x y h
-      apply FinitenessRelation.subrelation
-      exact h
-    · apply InvImage.wf
-      exact r.wf
-
-/--
-Internal implementation detail of the iterator library.
-The purpose of this class is that it implies a `Productive` instance but
-it is more convenient to implement.
--/
-structure ProductivenessRelation (α : Type w) (m : Type w → Type w') {β : Type w}
-    [Iterator α m β] where
-  rel : (IterM (α := α) m β) → (IterM (α := α) m β) → Prop
-  wf : WellFounded rel
-  subrelation : ∀ {it it'}, it'.IsPlausibleSkipSuccessorOf it → rel it' it
-
-theorem Productive.of_productivenessRelation
-    {α : Type w} {m : Type w → Type w'} {β : Type w}
-    [Iterator α m β] (r : ProductivenessRelation α m) : Productive α m where
-  wf := by
-    refine Subrelation.wf (r := r.rel) ?_ ?_
-    · intro x y h
-      apply ProductivenessRelation.subrelation
-      exact h
-    · apply InvImage.wf
-      exact r.wf
-
-end Std.Iterators

src/Init/Data/Iterators/Lemmas/Consumers.lean

@@ -9,3 +9,4 @@ prelude
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic
 public import Init.Data.Iterators.Lemmas.Consumers.Collect
 public import Init.Data.Iterators.Lemmas.Consumers.Loop
+public import Init.Data.Iterators.Lemmas.Consumers.Access

src/Init/Data/Iterators/Lemmas/Consumers/Access.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Consumers.Access
+
+namespace Std.Iter
+open Std.Iterators
+
+public theorem atIdxSlow?_eq_match [Iterator α Id β] [Productive α Id]
+    {n : Nat} {it : Iter (α := α) β} :
+    it.atIdxSlow? n =
+      (match it.step.val with
+      | .yield it' out =>
+        match n with
+        | 0 => some out
+        | n + 1 => it'.atIdxSlow? n
+      | .skip it' => it'.atIdxSlow? n
+      | .done => none) := by
+  fun_induction it.atIdxSlow? n <;> simp_all
+
+end Std.Iter

src/Init/Data/Iterators/PostconditionMonad.lean

@@ -287,6 +287,12 @@ theorem PostconditionT.run_attachLift {m : Type w → Type w'} [Monad m] [MonadA
     {x : m α} : (attachLift x).run = x := by
   simp [attachLift, run_eq_map, WeaklyLawfulMonadAttach.map_attach]
 
+@[simp]
+theorem PostconditionT.operation_attachLift {m : Type w → Type w'} [Monad m] [MonadAttach m]
+    {α : Type w} {x : m α} : (attachLift x : PostconditionT m α).operation =
+      MonadAttach.attach x := by
+  rfl
+
 instance {m : Type w → Type w'} {n : Type w → Type w''} [MonadLift m n] :
     MonadLift (PostconditionT m) (PostconditionT n) where
   monadLift x := ⟨_, monadLift x.operation⟩

src/Init/Data/Iterators/Producers/Monadic/List.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.Iterators.Consumers
-public import Init.Data.Iterators.Internal.Termination
 
 @[expose] public section
 
@@ -65,7 +64,7 @@ instance ListIterator.instIterator {α : Type w} [Pure m] : Iterator (ListIterat
 
 private def ListIterator.instFinitenessRelation [Pure m] :
     FinitenessRelation (ListIterator α) m where
-  rel := InvImage WellFoundedRelation.rel (ListIterator.list ∘ IterM.internalState)
+  Rel := InvImage WellFoundedRelation.rel (ListIterator.list ∘ IterM.internalState)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     simp_wf

src/Init/Data/List/Basic.lean

@@ -169,10 +169,10 @@ Examples:
   | a::as, b::bs, eqv => eqv a b && isEqv as bs eqv
   | _,     _,     _   => false
 
-@[simp] theorem isEqv_nil_nil : isEqv ([] : List α) [] eqv = true := rfl
-@[simp] theorem isEqv_nil_cons : isEqv ([] : List α) (a::as) eqv = false := rfl
-@[simp] theorem isEqv_cons_nil : isEqv (a::as : List α) [] eqv = false := rfl
-theorem isEqv_cons₂ : isEqv (a::as) (b::bs) eqv = (eqv a b && isEqv as bs eqv) := rfl
+@[simp, grind =] theorem isEqv_nil_nil : isEqv ([] : List α) [] eqv = true := rfl
+@[simp, grind =] theorem isEqv_nil_cons : isEqv ([] : List α) (a::as) eqv = false := rfl
+@[simp, grind =] theorem isEqv_cons_nil : isEqv (a::as : List α) [] eqv = false := rfl
+@[grind =] theorem isEqv_cons₂ : isEqv (a::as) (b::bs) eqv = (eqv a b && isEqv as bs eqv) := rfl
 
 
 /-! ## Lexicographic ordering -/

src/Init/Data/Nat/Gcd.lean

@@ -129,6 +129,9 @@ theorem gcd_assoc (m n k : Nat) : gcd (gcd m n) k = gcd m (gcd n k) :=
       (Nat.dvd_trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k)))
 instance : Std.Associative gcd := ⟨gcd_assoc⟩
 
+theorem gcd_left_comm (m n k : Nat) : gcd m (gcd n k) = gcd n (gcd m k) := by
+  rw [← gcd_assoc, ← gcd_assoc, gcd_comm m n]
+
 @[simp] theorem gcd_one_right (n : Nat) : gcd n 1 = 1 := (gcd_comm n 1).trans (gcd_one_left n)
 
 theorem gcd_mul_left (m n k : Nat) : gcd (m * n) (m * k) = m * gcd n k := by

src/Init/Data/Range/Polymorphic/RangeIterator.lean

@@ -6,7 +6,6 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Data.Iterators.Internal.Termination
 public import Init.Data.Iterators.Consumers.Access
 import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 public import Init.Data.Range.Polymorphic.PRange
@@ -232,7 +231,7 @@ private def List.length_filter_strict_mono {l : List α} {P Q : α → Bool} {a
 private def Iterator.instFinitenessRelation [UpwardEnumerable α] [LE α] [DecidableLE α]
     [LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] :
     FinitenessRelation (Rxc.Iterator α) Id where
-  rel it' it := it'.IsPlausibleSuccessorOf it
+  Rel it' it := it'.IsPlausibleSuccessorOf it
   wf := by
     constructor
     intro it
@@ -285,7 +284,7 @@ instance Iterator.instFinite [UpwardEnumerable α] [LE α] [DecidableLE α]
 private def Iterator.instProductivenessRelation [UpwardEnumerable α] [LE α] [DecidableLE α]
     [LawfulUpwardEnumerable α] :
     ProductivenessRelation (Rxc.Iterator α) Id where
-  rel := emptyWf.rel
+  Rel := emptyWf.rel
   wf := emptyWf.wf
   subrelation {it it'} h := by
     exfalso
@@ -808,7 +807,7 @@ private def List.length_filter_strict_mono {l : List α} {P Q : α → Bool} {a
 private def Iterator.instFinitenessRelation [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] :
     FinitenessRelation (Rxo.Iterator α) Id where
-  rel it' it := it'.IsPlausibleSuccessorOf it
+  Rel it' it := it'.IsPlausibleSuccessorOf it
   wf := by
     constructor
     intro it
@@ -861,7 +860,7 @@ instance Iterator.instFinite [UpwardEnumerable α] [LT α] [DecidableLT α]
 private def Iterator.instProductivenessRelation [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] :
     ProductivenessRelation (Rxo.Iterator α) Id where
-  rel := emptyWf.rel
+  Rel := emptyWf.rel
   wf := emptyWf.wf
   subrelation {it it'} h := by
     exfalso
@@ -1330,7 +1329,7 @@ theorem Iterator.isSome_next_of_isPlausibleIndirectOutput
 private def Iterator.instFinitenessRelation [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
     FinitenessRelation (Rxi.Iterator α) Id where
-  rel it' it := it'.IsPlausibleSuccessorOf it
+  Rel it' it := it'.IsPlausibleSuccessorOf it
   wf := by
     constructor
     intro it
@@ -1375,7 +1374,7 @@ instance Iterator.instFinite [UpwardEnumerable α]
 private def Iterator.instProductivenessRelation [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] :
     ProductivenessRelation (Rxi.Iterator α) Id where
-  rel := emptyWf.rel
+  Rel := emptyWf.rel
   wf := emptyWf.wf
   subrelation {it it'} h := by
     exfalso

src/Init/Data/Slice/Array/Iterator.lean

@@ -45,7 +45,7 @@ instance : Iterator (SubarrayIterator α) Id α where
   step it := pure <| .deflate ⟨SubarrayIterator.step it, rfl⟩
 
 private def SubarrayIterator.instFinitelessRelation : FinitenessRelation (SubarrayIterator α) Id where
-  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.xs.stop - it.internalState.xs.start)
+  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.xs.stop - it.internalState.xs.start)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     simp [IterM.IsPlausibleSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, step] at h

src/Init/Data/String/Decode.lean

@@ -1396,6 +1396,7 @@ scalar value.
 public def IsUTF8FirstByte (c : UInt8) : Prop :=
   c &&& 0x80 = 0 ∨ c &&& 0xe0 = 0xc0 ∨ c &&& 0xf0 = 0xe0 ∨ c &&& 0xf8 = 0xf0
 
+@[inline]
 public instance {c : UInt8} : Decidable c.IsUTF8FirstByte :=
   inferInstanceAs <| Decidable (c &&& 0x80 = 0 ∨ c &&& 0xe0 = 0xc0 ∨ c &&& 0xf0 = 0xe0 ∨ c &&& 0xf8 = 0xf0)
 

src/Init/Data/String/Pattern/Char.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.String.Pattern.Basic
-public import Init.Data.Iterators.Internal.Termination
 public import Init.Data.Iterators.Consumers.Monadic.Loop
 import Init.Data.String.Termination
 
@@ -59,7 +58,7 @@ instance (s : Slice) : Std.Iterator (ForwardCharSearcher c s) Id (SearchStep s)
         pure (.deflate ⟨.yield nextIt (.rejected currPos nextPos), by simp [h1, h2, nextIt, nextPos]⟩)
 
 def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharSearcher s c) Id where
-  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
+  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     simp_wf
@@ -124,7 +123,7 @@ instance (s : Slice) : Std.Iterator (BackwardCharSearcher s) Id (SearchStep s) w
         pure (.deflate ⟨.yield nextIt (.rejected nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩)
 
 def finitenessRelation : Std.Iterators.FinitenessRelation (BackwardCharSearcher s) Id where
-  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos.down)
+  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos.down)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     simp_wf

src/Init/Data/String/Pattern/Pred.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.String.Pattern.Basic
-public import Init.Data.Iterators.Internal.Termination
 public import Init.Data.Iterators.Consumers.Monadic.Loop
 import Init.Data.String.Termination
 
@@ -61,7 +60,7 @@ instance (s : Slice) : Std.Iterator (ForwardCharPredSearcher p s) Id (SearchStep
 
 
 def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharPredSearcher p s) Id where
-  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
+  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     simp_wf
@@ -134,7 +133,7 @@ instance (s : Slice) : Std.Iterator (BackwardCharPredSearcher s) Id (SearchStep
         pure (.deflate ⟨.yield nextIt (.rejected nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩)
 
 def finitenessRelation : Std.Iterators.FinitenessRelation (BackwardCharPredSearcher s) Id where
-  rel := InvImage WellFoundedRelation.rel
+  Rel := InvImage WellFoundedRelation.rel
       (fun it => it.internalState.currPos.offset.byteIdx)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by

src/Init/Data/String/Pattern/String.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.String.Pattern.Basic
-public import Init.Data.Iterators.Internal.Termination
 public import Init.Data.Iterators.Consumers.Monadic.Loop
 import Init.Data.String.Termination
 public import Init.Data.Vector.Basic
@@ -223,7 +222,7 @@ private instance : WellFoundedRelation (ForwardSliceSearcher s) where
 
 private def finitenessRelation :
     Std.Iterators.FinitenessRelation (ForwardSliceSearcher s) Id where
-  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState)
+  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     simp_wf

src/Init/Data/String/Slice.lean

@@ -165,7 +165,7 @@ private def toOption : SplitIterator pat s → Option (Std.Iter (α := σ s) (Se
 
 private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     Std.Iterators.FinitenessRelation (SplitIterator pat s) Id where
-  rel := InvImage (Option.lt Std.Iter.IsPlausibleSuccessorOf)
+  Rel := InvImage (Option.lt Std.Iter.IsPlausibleSuccessorOf)
     (SplitIterator.toOption ∘ Std.IterM.internalState)
   wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
   subrelation {it it'} h := by
@@ -256,7 +256,7 @@ private def toOption : SplitInclusiveIterator pat s → Option (Std.Iter (α :=
 
 private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     Std.Iterators.FinitenessRelation (SplitInclusiveIterator pat s) Id where
-  rel := InvImage (Option.lt Std.Iter.IsPlausibleSuccessorOf)
+  Rel := InvImage (Option.lt Std.Iter.IsPlausibleSuccessorOf)
     (SplitInclusiveIterator.toOption ∘ Std.IterM.internalState)
   wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
   subrelation {it it'} h := by
@@ -596,7 +596,7 @@ private def toOption : RevSplitIterator ρ s → Option (Std.Iter (α := σ s) (
 
 private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     Std.Iterators.FinitenessRelation (RevSplitIterator ρ s) Id where
-  rel := InvImage (Option.lt Std.Iter.IsPlausibleSuccessorOf)
+  Rel := InvImage (Option.lt Std.Iter.IsPlausibleSuccessorOf)
     (RevSplitIterator.toOption ∘ Std.IterM.internalState)
   wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
   subrelation {it it'} h := by
@@ -867,7 +867,7 @@ instance [Pure m] :
 
 private def finitenessRelation [Pure m] :
     Std.Iterators.FinitenessRelation (PosIterator s) m where
-  rel := InvImage WellFoundedRelation.rel
+  Rel := InvImage WellFoundedRelation.rel
       (fun it => s.utf8ByteSize - it.internalState.currPos.offset.byteIdx)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
@@ -949,7 +949,7 @@ instance [Pure m] :
 
 private def finitenessRelation [Pure m] :
     Std.Iterators.FinitenessRelation (RevPosIterator s) m where
-  rel := InvImage WellFoundedRelation.rel
+  Rel := InvImage WellFoundedRelation.rel
       (fun it => it.internalState.currPos.offset.byteIdx)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
@@ -1024,7 +1024,7 @@ instance [Pure m] : Std.Iterator ByteIterator m UInt8 where
 
 private def finitenessRelation [Pure m] :
     Std.Iterators.FinitenessRelation (ByteIterator) m where
-  rel := InvImage WellFoundedRelation.rel
+  Rel := InvImage WellFoundedRelation.rel
       (fun it => it.internalState.s.utf8ByteSize - it.internalState.offset.byteIdx)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
@@ -1104,7 +1104,7 @@ instance [Pure m] : Std.Iterator RevByteIterator m UInt8 where
 
 private def finitenessRelation [Pure m] :
     Std.Iterators.FinitenessRelation (RevByteIterator) m where
-  rel := InvImage WellFoundedRelation.rel
+  Rel := InvImage WellFoundedRelation.rel
       (fun it => it.internalState.offset.byteIdx)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by

src/Init/Data/Vector/Lemmas.lean

@@ -796,7 +796,8 @@ theorem getElem?_eq_none {xs : Vector α n} (h : n ≤ i) : xs[i]? = none := by
 
 -- This is a more aggressive pattern than for `List/Array.getElem?_eq_none`, because
 -- `length/size` won't appear.
-grind_pattern Vector.getElem?_eq_none => xs[i]?
+grind_pattern Vector.getElem?_eq_none => xs[i]? where
+  guard n ≤ i
 
 @[simp] theorem getElem?_eq_getElem {xs : Vector α n} {i : Nat} (h : i < n) : xs[i]? = some xs[i] :=
   getElem?_pos ..

src/Init/GetElem.lean

@@ -366,9 +366,11 @@ instance : GetElem? (List α) Nat α fun as i => i < as.length where
 theorem none_eq_getElem?_iff {l : List α} {i : Nat} : none = l[i]? ↔ length l ≤ i := by
   simp [eq_comm (a := none)]
 
-@[grind =]
 theorem getElem?_eq_none (h : length l ≤ i) : l[i]? = none := getElem?_eq_none_iff.mpr h
 
+grind_pattern getElem?_eq_none => l.length, l[i]? where
+  guard l.length ≤ i
+
 instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
   getElem?_def as i h := by
     split <;> simp_all

src/Init/MetaTypes.lean

@@ -36,6 +36,8 @@ inductive TransparencyMode where
   | reducible
   /-- Unfolds reducible constants and constants tagged with the `@[instance]` attribute. -/
   | instances
+  /-- Do not unfold anything -/
+  | none
   deriving Inhabited, BEq
 
 /-- Which structure types should eta be used with? -/

src/Init/Prelude.lean

@@ -375,6 +375,10 @@ theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ :
 theorem congrFun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : Eq f g) (a : α) : Eq (f a) (g a) :=
   h ▸ rfl
 
+/-- Similar to `congrFun` but `β` does not depend on `α`. -/
+theorem congrFun' {α : Sort u} {β : Sort v} {f g : α → β} (h : Eq f g) (a : α) : Eq (f a) (g a) :=
+  h ▸ rfl
+
 /-!
 Initialize the Quotient Module, which effectively adds the following definitions:
 ```

src/Init/Tactics.lean

@@ -369,6 +369,12 @@ In this setting all definitions that are not opaque are unfolded.
 -/
 syntax (name := withUnfoldingAll) "with_unfolding_all " tacticSeq : tactic
 
+/--
+`with_unfolding_none tacs` executes `tacs` using the `.none` transparency setting.
+In this setting no definitions are unfolded.
+-/
+syntax (name := withUnfoldingNone) "with_unfolding_none " tacticSeq : tactic
+
 /-- `first | tac | ...` runs each `tac` until one succeeds, or else fails. -/
 syntax (name := first) "first " withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
 

src/Lean.lean

@@ -44,7 +44,6 @@ public import Lean.LibrarySuggestions
 public import Lean.Namespace
 public import Lean.EnvExtension
 public import Lean.ErrorExplanation
-public import Lean.ErrorExplanations
 public import Lean.DefEqAttrib
 public import Lean.Shell
 public import Lean.ExtraModUses

src/Lean/Compiler/LCNF/Main.lean

@@ -4,16 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Compiler.Options
 public import Lean.Compiler.IR
 public import Lean.Compiler.LCNF.Passes
 public import Lean.Compiler.LCNF.ToDecl
 public import Lean.Compiler.LCNF.Check
-
+import Lean.Meta.Match.MatcherInfo
 public section
-
 namespace Lean.Compiler.LCNF
 /--
 We do not generate code for `declName` if

src/Lean/Compiler/LCNF/Specialize.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Compiler.LCNF.SpecInfo
 public import Lean.Compiler.LCNF.MonadScope
@@ -13,7 +12,7 @@ import Lean.Compiler.LCNF.Simp
 import Lean.Compiler.LCNF.ToExpr
 import Lean.Compiler.LCNF.Level
 import Lean.Compiler.LCNF.Closure
-
+import Lean.Meta.Transform
 namespace Lean.Compiler.LCNF
 namespace Specialize
 

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -4,13 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Compiler.InitAttr
 public import Lean.Compiler.LCNF.ToLCNF
-
+import Lean.Meta.Transform
+import Lean.Meta.Match.MatcherInfo
 public section
-
 namespace Lean.Compiler.LCNF
 /--
 Inline constants tagged with the `[macro_inline]` attribute occurring in `e`.

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.AppBuilder
 public import Lean.Compiler.CSimpAttr
@@ -12,9 +11,8 @@ public import Lean.Compiler.ImplementedByAttr
 public import Lean.Compiler.LCNF.Bind
 public import Lean.Compiler.NeverExtractAttr
 import Lean.Meta.CasesInfo
-
+import Lean.Meta.WHNF
 public section
-
 namespace Lean.Compiler.LCNF
 namespace ToLCNF
 

src/Lean/Data/PersistentHashMap.lean

@@ -193,6 +193,28 @@ partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α
 def findEntry? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option (α × β)
   | { root }, k => findEntryAux root (hash k |>.toUSize) k
 
+partial def findKeyDAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) (k₀ : α) : α :=
+  if h : i < keys.size then
+    let k' := keys[i]
+    if k == k' then k'
+    else findKeyDAtAux keys vals heq (i+1) k k₀
+  else k₀
+
+partial def findKeyDAux [BEq α] : Node α β → USize → α → α → α
+  | .entries entries, h, k, k₀ =>
+    let j     := (mod2Shift h shift).toNat
+    match entries[j]! with
+    | .null       => k₀
+    | .ref node   => findKeyDAux node (div2Shift h shift) k k₀
+    | .entry k' _ => if k == k' then k' else k₀
+  | .collision keys vals heq, _, k, k₀ => findKeyDAtAux keys vals heq 0 k k₀
+
+/--
+A more efficient `m.findEntry? a |>.map (·.1) |>.getD a₀`
+-/
+@[inline] def findKeyD {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) (a : α) (a₀ : α) : α :=
+  findKeyDAux m.root (hash a |>.toUSize) a a₀
+
 partial def containsAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Bool :=
   if h : i < keys.size then
     let k' := keys[i]

src/Lean/Data/PersistentHashSet.lean

@@ -45,6 +45,9 @@ variable {_ : BEq α} {_ : Hashable α}
   | some (a, _) => some a
   | none        => none
 
+@[inline] def findD (s : PersistentHashSet α) (a : α) (a₀ : α) : α :=
+  s.set.findKeyD a a₀
+
 @[inline] def contains (s : PersistentHashSet α) (a : α) : Bool :=
   s.set.contains a
 

src/Lean/Elab/ErrorExplanation.lean

@@ -84,19 +84,19 @@ def elabCheckedNamedError : TermElab := fun stx expType? => do
   addCompletionInfo <| CompletionInfo.errorName span partialId
   let name := id.getId.eraseMacroScopes
   pushInfoLeaf <| .ofErrorNameInfo { stx := id, errorName := name }
-  if let some explan := getErrorExplanationRaw? (← getEnv) name then
+  if let some explan ← getErrorExplanation? name then
     if let some removedVersion := explan.metadata.removedVersion? then
       logWarningAt id m!"The error name `{name}` was removed in Lean version {removedVersion} and \
         should not be used."
   else
-    logErrorAt id m!"There is no explanation associated with the name `{name}`. \
-      Add an explanation of this error to the `Lean.ErrorExplanations` module."
+    logErrorAt id m!"There is no explanation registered with the name `{name}`. \
+      Register an explanation for this error in the `Lean.ErrorExplanation` module."
   let stx' ← liftMacroM <| expandNamedErrorMacro stx
   elabTerm stx' expType?
 
 open Command in
 @[builtin_command_elab registerErrorExplanationStx] def elabRegisterErrorExplanation : CommandElab
-| `(registerErrorExplanationStx| $docStx:docComment register_error_explanation%$cmd $id:ident $t:term) => withRef cmd do
+| `(registerErrorExplanationStx| $_docStx register_error_explanation%$cmd $id:ident $t:term) => withRef cmd do
   unless (← getEnv).contains ``ErrorExplanation.Metadata do
     throwError "To use this command, add `import Lean.ErrorExplanation` to the header of this file"
   recordExtraModUseFromDecl ``ErrorExplanation.Metadata (isMeta := true)
@@ -116,18 +116,8 @@ open Command in
     throwErrorAt id m!"Invalid name `{name}`: Error explanation names must have two components"
       ++ .note m!"The first component of an error explanation name identifies the package from \
         which the error originates, and the second identifies the error itself."
-  runTermElabM fun _ => validateDocComment docStx
-  let doc ← getDocStringText docStx
   if errorExplanationExt.getState (← getEnv) |>.contains name then
     throwErrorAt id m!"Cannot add explanation: An error explanation already exists for `{name}`"
-  if let .error (lineOffset, msg) := ErrorExplanation.processDoc doc then
-    let some range := docStx.raw[1].getRange? | throwError msg
-    let fileMap ← getFileMap
-    let ⟨startLine, _⟩ := fileMap.toPosition range.start
-    let errLine := startLine + lineOffset
-    let synth := Syntax.ofRange { start := fileMap.ofPosition ⟨errLine, 0⟩,
-                                  stop  := fileMap.ofPosition ⟨errLine + 1, 0⟩ }
-    throwErrorAt synth msg
   let (declLoc? : Option DeclarationLocation) ← do
     let map ← getFileMap
     let start := id.raw.getPos?.getD 0
@@ -136,5 +126,5 @@ open Command in
       module := (← getMainModule)
       range := .ofStringPositions map start fin
     }
-  modifyEnv (errorExplanationExt.addEntry · (name, { metadata, doc, declLoc? }))
+  modifyEnv (errorExplanationExt.addEntry · (name, { doc := "", metadata, declLoc? }))
 | _ => throwUnsupportedSyntax

src/Lean/Elab/Tactic/BVDecide/External.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Std.Tactic.BVDecide.LRAT.Parser
 public import Lean.CoreM
+public import Std.Tactic.BVDecide.Syntax
 
 public section
 
@@ -146,7 +147,7 @@ solvers the solver is run with `timeout` in seconds as a maximum time limit to s
 Note: This function currently assume that the solver has the same CLI as CaDiCal.
 -/
 def satQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (proofOutput : System.FilePath)
-    (timeout : Nat) (binaryProofs : Bool) :
+    (timeout : Nat) (binaryProofs : Bool) (mode : Frontend.SolverMode) :
     CoreM SolverResult := do
   let cmd := solverPath.toString
   let mut args := #[
@@ -156,17 +157,12 @@ def satQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (pro
     s!"--binary={binaryProofs}",
     "--quiet",
     /-
-    This sets the magic parameters of cadical to optimize for UNSAT search.
-    Given the fact that we are mostly interested in proving things and expect user goals to be
-    provable this is a fine value to set
-    -/
-    "--unsat",
-    /-
     Bitwuzla sets this option and it does improve performance practically:
     https://github.com/bitwuzla/bitwuzla/blob/0e81e616af4d4421729884f01928b194c3536c76/src/sat/cadical.cpp#L34
     -/
     "--shrink=0"
   ]
+  args := args ++ solverModeFlags mode
 
   -- We implement timeouting ourselves because cadicals -t option is not available on Windows.
   let out? ← runInterruptible timeout { cmd, args, stdin := .piped, stdout := .piped, stderr := .null }
@@ -190,6 +186,12 @@ def satQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (pro
           throwError s!"Error {err} while parsing:\n{stdout}"
       else
         throwError s!"The external prover produced unexpected output, stdout:\n{stdout}stderr:\n{stderr}"
+where
+  solverModeFlags (mode : Frontend.SolverMode) : Array String :=
+    match mode with
+    | .proof => #["--unsat"]
+    | .counterexample => #["--sat"]
+    | .default => #["--default"]
 
 end External
 

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

@@ -344,7 +344,14 @@ def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : Ref
 
   let res ←
     withTraceNode `Meta.Tactic.sat (fun _ => return "Obtaining external proof certificate") do
-      runExternal cnf ctx.solver ctx.lratPath ctx.config.trimProofs ctx.config.timeout ctx.config.binaryProofs
+      runExternal
+        cnf
+        ctx.solver
+        ctx.lratPath
+        ctx.config.trimProofs
+        ctx.config.timeout
+        ctx.config.binaryProofs
+        ctx.config.solverMode
 
   match res with
   | .ok cert =>

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

@@ -4,13 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 module
-
 prelude
 public import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.Reflect
 public import Std.Tactic.BVDecide.Reflect
-
+import Lean.Meta.LitValues
 public section
-
 /-!
 Provides the logic for reifying `BitVec` expressions.
 -/

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

@@ -4,10 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 module
-
 prelude
 public import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.ReifiedLemmas
-
+import Lean.Meta.LitValues
 public section
 
 /-!

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

@@ -131,7 +131,7 @@ Run an external SAT solver on the `CNF` to obtain an LRAT proof.
 This will obtain an `LratCert` if the formula is UNSAT and throw errors otherwise.
 -/
 def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.FilePath)
-    (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool) :
+    (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool) (solverMode : Frontend.SolverMode) :
     CoreM (Except (Array (Bool × Nat)) LratCert) := do
   IO.FS.withTempFile fun cnfHandle cnfPath => do
     withTraceNode `Meta.Tactic.sat (fun _ => return "Serializing SAT problem to DIMACS file") do
@@ -141,7 +141,7 @@ def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.Fi
 
     let res ←
       withTraceNode `Meta.Tactic.sat (fun _ => return "Running SAT solver") do
-        External.satQuery solver cnfPath lratPath timeout binaryProofs
+        External.satQuery solver cnfPath lratPath timeout binaryProofs solverMode
     if let .sat assignment := res then
       return .error assignment
 

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

@@ -195,16 +195,16 @@ where
       return false
 
     let ctorTyp := (← getConstInfoCtor constInfo.ctors.head!).type
-    let analyzer state arg := do return state || (← typeCasesRelevant (← arg.fvarId!.getType))
-    let interesting ← forallTelescope ctorTyp fun args _ => args.foldlM (init := false) analyzer
+    let interesting ← forallTelescope ctorTyp fun args _ =>
+      -- Note: Important not to short circuit here so that we collect information about all
+      -- arguments in case we want to split recursively.
+      args.foldlM (init := false) fun state arg => do
+        return state || (← typeCasesRelevant (← arg.fvarId!.getType))
     return interesting
 
   typeCasesRelevant (expr : Expr) : PreProcessM Bool := do
-    match_expr expr with
-    | BitVec n => return (← getNatValue? n).isSome
-    | _ =>
-      let some const := expr.getAppFn.constName? | return false
-      analyzeConst const
+    let some const := expr.getAppFn.constName? | return false
+    analyzeConst const
 
 end Frontend.Normalize
 end Lean.Elab.Tactic.BVDecide

src/Lean/Elab/Tactic/Do/Attr.lean

@@ -193,7 +193,7 @@ def mkSpecTheoremFromStx (ref : Syntax) (proof : Expr) (prio : Nat := eval_prio
   mkSpecTheorem type (.stx (← mkFreshId) ref proof) prio
 
 def addSpecTheoremEntry (d : SpecTheorems) (e : SpecTheorem) : SpecTheorems :=
-  { d with specs := d.specs.insertCore e.keys e }
+  { d with specs := d.specs.insertKeyValue e.keys e }
 
 def addSpecTheorem (ext : SpecExtension) (declName : Name) (prio : Nat) (attrKind : AttributeKind) : MetaM Unit := do
   let thm ← mkSpecTheoremFromConst declName prio

src/Lean/Elab/Tactic/Do/VCGen.lean

@@ -436,7 +436,7 @@ where
     let some tactic := tactic | return vcs
     let mut newVCs := #[]
     for vc in vcs do
-      let vcs ← try evalTacticAt tactic vc catch _ => pure [vc]
+      let vcs ← evalTacticAt tactic vc
       newVCs := newVCs ++ vcs
     return newVCs
 

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -320,6 +320,9 @@ def evalApplyLikeTactic (tac : MVarId → Expr → MetaM (List MVarId)) (e : Syn
 @[builtin_tactic Lean.Parser.Tactic.withUnfoldingAll] def evalWithUnfoldingAll : Tactic := fun stx =>
   withTransparency TransparencyMode.all <| evalTactic stx[1]
 
+@[builtin_tactic Lean.Parser.Tactic.withUnfoldingNone] def evalWithUnfoldingNone : Tactic := fun stx =>
+  withTransparency TransparencyMode.none <| evalTactic stx[1]
+
 /--
   Elaborate `stx`. If it is a free variable, return it. Otherwise, assert it, and return the free variable.
   Note that, the main goal is updated when `Meta.assert` is used in the second case. -/

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -22,8 +22,9 @@ structure Context extends Tactic.Context where
 open Meta.Grind (Goal)
 
 structure State where
-  state : Meta.Grind.State
-  goals : List Goal
+  symState   : Meta.Sym.State
+  grindState : Meta.Grind.State
+  goals      : List Goal
 
 structure SavedState where
   term   : Term.SavedState
@@ -288,8 +289,8 @@ open Grind
 def liftGrindM (k : GrindM α) : GrindTacticM α := do
   let ctx ← read
   let s ← get
-  let (a, state) ← liftMetaM <| (Grind.withGTransparency k) ctx.methods.toMethodsRef ctx.ctx |>.run s.state
-  modify fun s => { s with state }
+  let ((a, grindState), symState) ← liftMetaM <| StateRefT'.run ((Grind.withGTransparency k) ctx.methods.toMethodsRef ctx.ctx |>.run s.grindState) s.symState
+  modify fun s => { s with grindState, symState }
   return a
 
 def replaceMainGoal (goals : List Goal) : GrindTacticM Unit := do
@@ -358,15 +359,17 @@ def mkEvalTactic' (elaborator : Name) (params : Params) : TermElabM (Goal → TS
     let methods ← getMethods
     let grindCtx ← readThe Meta.Grind.Context
     let grindState ← get
+    let symState ← getThe Sym.State
     -- **Note**: we discard changes to `Term.State`
-    let (subgoals, grindState') ← Term.TermElabM.run' (ctx := termCtx) (s := termState) do
+    let (subgoals, grindState', symState') ← Term.TermElabM.run' (ctx := termCtx) (s := termState) do
       let (_, s) ← GrindTacticM.run
             (ctx := { recover := false, methods, ctx := grindCtx, params, elaborator })
-            (s := { state := grindState, goals := [goal] }) do
+            (s := { grindState, symState, goals := [goal] }) do
         evalGrindTactic stx.raw
         pruneSolvedGoals
-      return (s.goals, s.state)
+      return (s.goals, s.grindState, s.symState)
     set grindState'
+    set symState'
     return subgoals
   return eval
 
@@ -389,8 +392,9 @@ def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM
       let ctx ← readThe Meta.Grind.Context
       /- Restore original config -/
       let ctx := { ctx with config := params.config }
-      let state ← get
-      pure (methods, ctx, { state, goals })
+      let grindState ← get
+      let symState ← getThe Sym.State
+      return (methods, ctx, { grindState, symState, goals })
   let tctx ← read
   k { tctx with methods, ctx, params } |>.run state
 

src/Lean/Elab/Tactic/Grind/LintExceptions.lean

@@ -15,6 +15,7 @@ import Lean.Elab.Tactic.Grind.Lint
 #grind_lint skip List.replicate_sublist_iff
 #grind_lint skip List.Sublist.append
 #grind_lint skip List.Sublist.middle
+#grind_lint skip List.getLast?_pmap
 #grind_lint skip Array.count_singleton
 #grind_lint skip Array.foldl_empty
 #grind_lint skip Array.foldr_empty

src/Lean/Elab/Tactic/Guard.lean

@@ -67,6 +67,7 @@ def MatchKind.toStringDescr : MatchKind → String
   | .defEq .all => s!"definitionally equal (unfolding all constants) to"
   | .defEq .reducible => s!"definitionally equal (unfolding reducible constants) to"
   | .defEq .instances => s!"definitionally equal (unfolding instances) to"
+  | .defEq .none => s!"definitionally equal (not unfolding any constants) to"
   | .alphaEq => "alpha-equivalent to"
 
 /-- Elaborate `a` and `b` and then do the given equality test `mk`. We make sure to unify

src/Lean/Elab/Tactic/Induction.lean

@@ -12,7 +12,6 @@ public import Lean.Elab.Tactic.ElabTerm
 import Lean.Meta.Tactic.FunIndCollect
 import Lean.Elab.App
 import Lean.Elab.Tactic.Generalize
-import Lean.ErrorExplanations.InductionWithNoAlts
 
 
 public section

src/Lean/Elab/Tactic/Injection.lean

@@ -4,12 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Injection
 public import Lean.Meta.Tactic.Assumption
 public import Lean.Elab.Tactic.ElabTerm
-
 public section
 namespace Lean.Elab.Tactic
 

src/Lean/Elab/Tactic/Monotonicity.lean

@@ -29,7 +29,7 @@ partial def headBetaUnderLambda (f : Expr) : Expr := Id.run do
 builtin_initialize monotoneExt :
     SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ←
   registerSimpleScopedEnvExtension {
-    addEntry := fun dt (n, ks) => dt.insertCore ks n
+    addEntry := fun dt (n, ks) => dt.insertKeyValue ks n
     initial := {}
   }
 

src/Lean/EnvExtension.lean

@@ -105,9 +105,13 @@ instance : Inhabited TagDeclarationExtension :=
   inferInstanceAs (Inhabited (SimplePersistentEnvExtension Name NameSet))
 
 def tag (ext : TagDeclarationExtension) (env : Environment) (declName : Name) : Environment :=
-  have : Inhabited Environment := ⟨env⟩
-  assert! env.getModuleIdxFor? declName |>.isNone -- See comment at `TagDeclarationExtension`
-  ext.addEntry (asyncDecl := declName) env declName
+  if declName.isAnonymous then
+    -- This case might happen on partial elaboration; ignore instead of triggering any panics below
+    env
+  else
+    have : Inhabited Environment := ⟨env⟩
+    assert! env.getModuleIdxFor? declName |>.isNone -- See comment at `TagDeclarationExtension`
+    ext.addEntry (asyncDecl := declName) env declName
 
 def isTagged (ext : TagDeclarationExtension) (env : Environment) (declName : Name)
     (asyncMode := ext.toEnvExtension.asyncMode) : Bool :=

src/Lean/ErrorExplanation.lean

@@ -40,288 +40,18 @@ Error explanations are rendered in the manual; a link to the resulting manual pa
 the bottom of corresponding error messages thrown using `throwNamedError` or `throwNamedErrorAt`.
 -/
 structure ErrorExplanation where
+  /-- The `doc` field is deprecated and should always be the empty string -/
   doc : String
   metadata : ErrorExplanation.Metadata
   declLoc? : Option DeclarationLocation
 
-namespace ErrorExplanation
-
 /--
 Returns the error explanation summary prepended with its severity. For use in completions and
 hovers.
 -/
-def summaryWithSeverity (explan : ErrorExplanation) : String :=
+def ErrorExplanation.summaryWithSeverity (explan : ErrorExplanation) : String :=
   s!"({explan.metadata.severity}) {explan.metadata.summary}"
 
-/--
-The kind of a code block in an error explanation example. `broken` blocks raise the diagnostic being
-explained; `fixed` blocks must compile successfully.
--/
-inductive CodeInfo.Kind
-  | broken | fixed
-  deriving Repr, Inhabited, BEq
-
-instance : ToString CodeInfo.Kind where
-  toString
-  | .broken => "broken"
-  | .fixed => "fixed"
-
-def CodeInfo.Kind.ofString : String → Option CodeInfo.Kind
-  | "broken" => some .broken
-  | "fixed" => some .fixed
-  | _ => none
-
-/-- Metadata about a code block in an error explanation, parsed from the block's info string. -/
-structure CodeInfo where
-  lang : String
-  kind? : Option CodeInfo.Kind
-  title? : Option String
-deriving Repr
-
-open Std.Internal Parsec Parsec.String in
-/-- Parse metadata for an error explanation code block from its info string. -/
-def CodeInfo.parse (s : String) : Except String CodeInfo :=
-  infoString.run s |>.mapError (fun e => s!"Invalid code block info string `{s}`: {e}")
-where
-  /-- Parses the contents of a string literal up to, but excluding, the closing quotation mark. -/
-  stringContents : Parser String := attempt do
-    let escaped := pchar '\\' *> pchar '"'
-    let cs ← many (notFollowedBy (pchar '"') *> (escaped <|> any))
-    return String.ofList cs.toList
-
-  /--
-  Parses all input up to the next whitespace. If `nonempty` is `true`, fails if there is no input
-  prior to the next whitespace.
-  -/
-  upToWs (nonempty : Bool) : Parser String := fun it =>
-    let it' := (it.2.find? fun (c : Char) => c.isWhitespace).getD it.1.endPos
-    if nonempty && it' == it.2 then
-      .error ⟨_, it'⟩ (.other "Expected a nonempty string")
-    else
-      .success ⟨_, it'⟩ (it.1.slice! it.2 it').copy
-
-  /-- Parses a named attribute, and returns its name and value. -/
-  namedAttr : Parser (String × String) := attempt do
-    let name ← skipChar '(' *> ws *> (upToWs true)
-    let contents ← ws *> skipString ":=" *> ws *> skipChar '"' *> stringContents
-    discard <| skipChar '"' *> ws *> skipChar ')'
-    return (name, contents)
-
-  /--
-  Parses an "attribute" in an info string, either a space-delineated identifier or a named
-  attribute of the form `(name := "value")`.
-  -/
-  attr : Parser (String ⊕ String × String) :=
-    .inr <$> namedAttr <|> .inl <$> (upToWs true)
-
-  infoString : Parser CodeInfo := do
-    let lang ← upToWs false
-    let attrs ← many (attempt <| ws *> attr)
-    let mut kind? := Option.none
-    let mut title? := Option.none
-    for attr in attrs do
-      match attr with
-      | .inl atomicAttr =>
-        match atomicAttr with
-        | "broken" | "fixed" =>
-          match kind? with
-          | none => kind? := Kind.ofString atomicAttr
-          | some kind =>
-            fail s!"Redundant kind specifications: previously `{kind}`; now `{atomicAttr}`"
-        | _ => fail s!"Invalid attribute `{atomicAttr}`"
-      | .inr (name, val) =>
-        if name == "title" then
-          if title?.isNone then
-            title? := some val
-          else
-            fail "Redundant title specifications"
-        else
-          fail s!"Invalid named attribute `{name}`; expected `title`"
-    return { lang, title?, kind? }
-
-open Std.Internal Parsec
-
-/--
-An iterator storing nonempty lines in an error explanation together with their original line
-numbers.
--/
-private structure ValidationState where
-  lines : Array (String × Nat)
-  idx   : Nat := 0
-deriving Repr, Inhabited
-
-/-- Creates an iterator for validation from the raw contents of an error explanation. -/
-private def ValidationState.ofSource (input : String) : ValidationState where
-  lines := input.split '\n'
-    |>.filter (!·.trimAscii.isEmpty)
-    |>.toStringArray
-    |>.zipIdx
-
--- Workaround to account for the fact that `Input` expects "EOF" to be a valid position
-private def ValidationState.get (s : ValidationState) :=
-  if _ : s.idx < s.lines.size then
-    s.lines[s.idx].1
-  else
-    ""
-
-private def ValidationState.getLineNumber (s : ValidationState) :=
-  if _ : s.lines.size = 0 then
-    0
-  else
-    s.lines[min s.idx (s.lines.size - 1)].2
-
-private instance : Input ValidationState String Nat where
-  pos := ValidationState.idx
-  next := fun s => { s with idx := min (s.idx + 1) s.lines.size }
-  curr := ValidationState.get
-  hasNext := fun s => s.idx < s.lines.size
-  next' := fun s _ => { s with idx := s.idx + 1 }
-  curr' := fun s _ => s.get
-
-private abbrev ValidationM := Parsec ValidationState
-
-private def ValidationM.run (p : ValidationM α) (input : String) : Except (Nat × String) α :=
-  match p (.ofSource input) with
-  | .success _ res => Except.ok res
-  | .error s err  => Except.error (s.getLineNumber, toString err)
-
-/--
-Matches `p` as many times as possible, followed by EOF. If `p` cannot be matched prior to the end
-of the input, rethrows the corresponding error.
--/
-private partial def manyThenEOF (p : ValidationM α) : ValidationM Unit := fun s =>
-  match eof s with
-  | .success .. => .success s ()
-  | .error .. =>
-    match p s with
-    | .success s' _ => manyThenEOF p s'
-    | .error s' err => .error s' err
-
-/-- Repeatedly parses the next input as long as it satisfies `p`, and discards the result. -/
-private partial def manyD (p : ValidationM α) : ValidationM Unit :=
-  Parsec.tryCatch p (fun _ => manyD p) (fun _ => pure ())
-
-/-- Parses one or more inputs as long as they satisfy `p`, and discards the result. -/
-private def many1D (p : ValidationM α) : ValidationM Unit :=
-  p *> manyD p
-
-/-- Repeatedly parses the next input as long as it fails to satisfy `p`, and discards the result. -/
-private def manyNotD (p : ValidationM α) : ValidationM Unit :=
-  manyD (notFollowedBy p *> skip)
-
-/-- Parses an error explanation: a general description followed by an examples section. -/
-private def parseExplanation : ValidationM Unit := do
-  manyNotD examplesHeader
-  eof <|> (examplesHeader *> manyThenEOF singleExample)
-where
-  /-- The top-level `# Examples` header -/
-  examplesHeader := attempt do
-    let line ← any
-    if (matchHeader 1 "Examples" line).isSome then
-      return
-    else
-      fail s!"Expected level-1 'Examples' header, but found `{line}`"
-
-  -- We needn't `attempt` examples because they never appear in a location where backtracking is
-  -- possible, and persisting the line index allows better error message placement
-  singleExample := do
-    let header ← exampleHeader
-    labelingExampleErrors header do
-      codeBlock "lean" (some .broken)
-      many1D (codeBlock "output")
-      many1D do
-        let leanBlock ← codeBlock "lean" (some .fixed)
-        let outputBlocks ← many (codeBlock "output")
-        return (leanBlock, outputBlocks)
-      manyNotD exampleEndingHeader
-
-  /-- A level-2 header for a single example. -/
-  exampleHeader := attempt do
-    let line ← any
-    if let some header := matchHeader 2 none line then
-      return header
-    else
-      fail s!"Expected level-2 header for an example section, but found `{line}`"
-
-  /-- A header capable of ending an example. -/
-  exampleEndingHeader := attempt do
-    let line ← any
-    if (matchHeader 1 none line).isSome || (matchHeader 2 none line).isSome then
-      return
-    else
-      fail s!"Expected a level-1 or level-2 header, but found `{line}`"
-
-  codeBlock (lang : String) (kind? : Option ErrorExplanation.CodeInfo.Kind := none) := attempt do
-    let (numTicks, infoString) ← fence
-      <|> fail s!"Expected a(n){kind?.map (s!" {·}") |>.getD ""} `{lang}` code block"
-    manyD (notFollowedBy (fence numTicks) *> any)
-    let (_, closing) ← fence numTicks
-      <|> fail s!"Missing closing code fence for block with header '{infoString}'"
-    -- Validate code block:
-    unless closing.trimAscii.isEmpty do
-      fail s!"Expected a closing code fence, but found the nonempty info string `{closing}`"
-    let info ← match ErrorExplanation.CodeInfo.parse infoString.copy with
-      | .ok i => pure i
-      | .error s =>
-        fail s
-    let langMatches := info.lang == lang
-    let kindMatches := (kind?.map (some · == info.kind?)).getD true
-    unless langMatches && kindMatches do
-      let (expKind, actKind) := match kind? with
-        | some kind =>
-          let actualKindStr := (info.kind?.map (s!" {·}")).getD " unspecified-kind"
-          (s!" {kind}", actualKindStr)
-        | none => ("", "")
-      fail s!"Expected a(n){expKind} `{lang}` code block, but found a(n){actKind} `{info.lang}` one"
-
-  fence (ticksToClose : Option Nat := none) := attempt do
-    let line ← any
-    if line.startsWith "```" then
-      let numTicks := line.takeWhile (· == '`') |>.utf8ByteSize -- this makes sense because we know the slice consists only of ticks
-      match ticksToClose with
-      | none => return (numTicks, line.drop numTicks)
-      | some n =>
-        if numTicks == n then
-          return (numTicks, line.drop numTicks)
-        else
-          fail s!"Expected a closing code fence with {n} ticks, but found:\n{line}"
-    else
-      -- Don't put `line` in backticks here because it might be a partial code fence
-      fail s!"Expected a code fence, but found:\n{line}"
-
-  /-- Prepends an error raised by `x` to indicate that it arose in example `header`. -/
-  labelingExampleErrors {α} (header : String) (x : ValidationM α) : ValidationM α := fun s =>
-    match x s with
-    | res@(.success ..) => res
-    | .error s' msg => .error s' (.other s!"Example '{header}' is malformed: {msg}")
-
-  /--
-  If `line` is a level-`level` header and, if `title?` is non-`none`, its title is `title?`,
-  then returns the contents of the header at `line` (i.e., stripping the leading `#`). Returns
-  `none` if `line` is not a header of the appropriate form.
-  -/
-  matchHeader (level : Nat) (title? : Option String) (line : String) : Option String := do
-    let octsEndPos := String.Pos.Raw.nextWhile line (· == '#') 0
-    guard (octsEndPos.byteIdx == level)
-    guard (octsEndPos.get line == ' ')
-    let titleStartPos := octsEndPos.next line
-    let title := Substring.Raw.mk line titleStartPos line.rawEndPos |>.toString
-    let titleMatches : Bool := match title? with
-      | some expectedTitle => title == expectedTitle
-      | none => true
-    guard titleMatches
-    some title
-
-/--
-Validates that the given error explanation has the expected structure. If an error is found, it is
-represented as a pair `(lineNumber, errorMessage)` where `lineNumber` gives the 0-based offset from
-the first line of `doc` at which the error occurs.
--/
-def processDoc (doc : String) : Except (Nat × String) Unit :=
-  parseExplanation.run doc
-
-end ErrorExplanation
-
 /-- An environment extension that stores error explanations.  -/
 builtin_initialize errorExplanationExt : SimplePersistentEnvExtension (Name × ErrorExplanation) (NameMap ErrorExplanation) ←
   registerSimplePersistentEnvExtension {
@@ -332,44 +62,126 @@ builtin_initialize errorExplanationExt : SimplePersistentEnvExtension (Name × E
           acc.insert n v
   }
 
-/-- Returns an error explanation for the given name if one exists, rewriting manual links. -/
-def getErrorExplanation? [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (name : Name) : m (Option ErrorExplanation) := do
-  let explan? := errorExplanationExt.getState (← getEnv) |>.find? name
-  explan?.mapM fun explan =>
-    return { explan with doc := (← rewriteManualLinks explan.doc) }
+/-- Returns an error explanation for the given name if one exists. -/
+def getErrorExplanation? [Monad m] [MonadEnv m] (name : Name) : m (Option ErrorExplanation) := do
+  return errorExplanationExt.getState (← getEnv) |>.find? name
 
-/--
-Returns an error explanation for the given name if one exists *without* rewriting manual links.
-
-In general, use `Lean.getErrorExplanation?` instead if the body of the explanation will be used.
--/
+@[deprecated getErrorExplanation? (since := "2026-12-20")]
 def getErrorExplanationRaw? (env : Environment) (name : Name) : Option ErrorExplanation := do
   errorExplanationExt.getState env |>.find? name
 
 /-- Returns `true` if there exists an error explanation named `name`. -/
-def hasErrorExplanation [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (name : Name) : m Bool :=
+def hasErrorExplanation [Monad m] [MonadEnv m] (name : Name) : m Bool :=
   return errorExplanationExt.getState (← getEnv) |>.contains name
 
-/--
-Returns all error explanations with their names as an unsorted array, *without* rewriting manual
-links.
+/-- Returns all error explanations with their names, sorted by name. -/
+public def getErrorExplanations [Monad m] [MonadEnv m] : m (Array (Name × ErrorExplanation)) := do
+  return errorExplanationExt.getState (← getEnv)
+    |>.toArray
+    |>.qsort fun e e' => e.1.toString < e'.1.toString
 
-In general, use `Lean.getErrorExplanations` or `Lean.getErrorExplanationsSorted` instead of this
-function if the bodies of the fetched explanations will be used.
--/
-def getErrorExplanationsRaw (env : Environment) : Array (Name × ErrorExplanation) :=
-  errorExplanationExt.getState env |>.toArray
+@[deprecated getErrorExplanations (since := "2026-12-20")]
+public def getErrorExplanationsRaw (env : Environment) : Array (Name × ErrorExplanation) :=
+  errorExplanationExt.getState env
+    |>.toArray
+    |>.qsort fun e e' => e.1.toString < e'.1.toString
 
-/-- Returns all error explanations with their names, rewriting manual links. -/
-def getErrorExplanations [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] : m (Array (Name × ErrorExplanation)) := do
-  let entries := errorExplanationExt.getState (← getEnv) |>.toArray
-  entries
-    |>.mapM fun (n, e) => return (n, { e with doc := (← rewriteManualLinks e.doc) })
-
-/--
-Returns all error explanations with their names as a sorted array, rewriting manual links.
--/
-def getErrorExplanationsSorted [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] : m (Array (Name × ErrorExplanation)) := do
-  return (← getErrorExplanations).qsort fun e e' => e.1.toString < e'.1.toString
+@[deprecated getErrorExplanations (since := "2026-12-20")]
+public def getErrorExplanationsSorted [Monad m] [MonadEnv m] : m (Array (Name × ErrorExplanation)) := do
+  getErrorExplanations
 
 end Lean
+
+/-
+Error explanations registered in the compiler must be added to the manual and
+referenced in the Manual.ErrorExplanations module here:
+
+https://github.com/leanprover/reference-manual/blob/main/Manual/ErrorExplanations.lean
+
+Details:
+https://github.com/leanprover/reference-manual/blob/main/Manual/ErrorExplanations/README.md
+-/
+
+/-- -/
+register_error_explanation lean.ctorResultingTypeMismatch {
+  summary := "Resulting type of constructor was not the inductive type being declared."
+  sinceVersion := "4.22.0"
+}
+
+/-- -/
+register_error_explanation lean.dependsOnNoncomputable {
+  summary := "Declaration depends on noncomputable definitions but is not marked as noncomputable"
+  sinceVersion := "4.22.0"
+}
+
+/-- -/
+register_error_explanation lean.inductionWithNoAlts {
+  summary := "Induction pattern with nontactic in natural-number-game-style `with` clause."
+  sinceVersion := "4.26.0"
+}
+
+/-- -/
+register_error_explanation lean.inductiveParamMismatch {
+  summary := " Invalid parameter in an occurrence of an inductive type in one of its constructors."
+  sinceVersion := "4.22.0"
+}
+
+/-- -/
+register_error_explanation lean.inductiveParamMissing {
+  summary := "Parameter not present in an occurrence of an inductive type in one of its constructors."
+  sinceVersion := "4.22.0"
+}
+
+/-- -/
+register_error_explanation lean.inferBinderTypeFailed {
+  summary := "The type of a binder could not be inferred."
+  sinceVersion := "4.23.0"
+}
+
+/-- -/
+register_error_explanation lean.inferDefTypeFailed {
+  summary := "The type of a definition could not be inferred."
+  sinceVersion := "4.23.0"
+}
+
+/-- -/
+register_error_explanation lean.invalidDottedIdent {
+  summary := "Dotted identifier notation used with invalid or non-inferrable expected type."
+  sinceVersion := "4.22.0"
+}
+
+/-- -/
+register_error_explanation lean.invalidField {
+  summary := "Generalized field notation used in a potentially ambiguous way."
+  sinceVersion := "4.22.0"
+}
+
+/-- -/
+register_error_explanation lean.projNonPropFromProp {
+  summary := "Tried to project data from a proof."
+  sinceVersion := "4.23.0"
+}
+
+/-- -/
+register_error_explanation lean.propRecLargeElim {
+  summary := "Attempted to eliminate a proof into a higher type universe."
+  sinceVersion := "4.23.0"
+}
+
+/-- -/
+register_error_explanation lean.redundantMatchAlt {
+  summary := "Match alternative will never be reached."
+  sinceVersion := "4.22.0"
+}
+
+/-- -/
+register_error_explanation lean.synthInstanceFailed {
+  summary := "Failed to synthesize instance of type class."
+  sinceVersion := "4.26.0"
+}
+
+/-- -/
+register_error_explanation lean.unknownIdentifier {
+  summary := "Failed to resolve identifier to variable or constant."
+  sinceVersion := "4.23.0"
+}

src/Lean/ErrorExplanations.lean

@@ -1,22 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanations.CtorResultingTypeMismatch
-public import Lean.ErrorExplanations.DependsOnNoncomputable
-public import Lean.ErrorExplanations.InductionWithNoAlts
-public import Lean.ErrorExplanations.InductiveParamMismatch
-public import Lean.ErrorExplanations.InductiveParamMissing
-public import Lean.ErrorExplanations.InferBinderTypeFailed
-public import Lean.ErrorExplanations.InferDefTypeFailed
-public import Lean.ErrorExplanations.InvalidDottedIdent
-public import Lean.ErrorExplanations.InvalidField
-public import Lean.ErrorExplanations.ProjNonPropFromProp
-public import Lean.ErrorExplanations.PropRecLargeElim
-public import Lean.ErrorExplanations.RedundantMatchAlt
-public import Lean.ErrorExplanations.SynthInstanceFailed
-public import Lean.ErrorExplanations.UnknownIdentifier

src/Lean/ErrorExplanations/CtorResultingTypeMismatch.lean

@@ -1,72 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-In an inductive declaration, the resulting type of each constructor must match the type being
-declared; if it does not, this error is raised. That is, every constructor of an inductive type must
-return a value of that type. See the [Inductive Types](lean-manual://section/inductive-types) manual
-section for additional details. Note that it is possible to omit the resulting type for a
-constructor if the inductive type being defined has no indices.
-
-# Examples
-
-## Typo in Resulting Type
-```lean broken
-inductive Tree (α : Type) where
-  | leaf : Tree α
-  | node : α → Tree α → Treee α
-```
-```output
-Unexpected resulting type for constructor `Tree.node`: Expected an application of
-  Tree
-but found
-  ?m.2
-```
-```lean fixed
-inductive Tree (α : Type) where
-  | leaf : Tree α
-  | node : α → Tree α → Tree α
-```
-
-## Missing Resulting Type After Constructor Parameter
-
-```lean broken
-inductive Credential where
-  | pin      : Nat
-  | password : String
-```
-```output
-Unexpected resulting type for constructor `Credential.pin`: Expected
-  Credential
-but found
-  Nat
-```
-```lean fixed (title := "Fixed (resulting type)")
-inductive Credential where
-  | pin      : Nat → Credential
-  | password : String → Credential
-```
-```lean fixed (title := "Fixed (named parameter)")
-inductive Credential where
-  | pin (num : Nat)
-  | password (str : String)
-```
-
-If the type of a constructor is annotated, the full type—including the resulting type—must be
-provided. Alternatively, constructor parameters can be written using named binders; this allows the
-omission of the constructor's resulting type because it contains no indices.
--/
-register_error_explanation lean.ctorResultingTypeMismatch {
-  summary := "Resulting type of constructor was not the inductive type being declared."
-  sinceVersion := "4.22.0"
-}

src/Lean/ErrorExplanations/DependsOnNoncomputable.lean

@@ -1,122 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error indicates that the specified definition depends on one or more definitions that do not
-contain executable code and is therefore required to be marked as `noncomputable`. Such definitions
-can be type-checked but do not contain code that can be executed by Lean.
-
-If you intended for the definition named in the error message to be noncomputable, marking it as
-`noncomputable` will resolve this error. If you did not, inspect the noncomputable definitions on
-which it depends: they may be noncomputable because they failed to compile, are `axiom`s, or were
-themselves marked as `noncomputable`. Making all of your definition's noncomputable dependencies
-computable will also resolve this error. See the manual section on
-[Modifiers](lean-manual://section/declaration-modifiers) for more information about noncomputable
-definitions.
-
-# Examples
-
-## Necessarily Noncomputable Function Not Appropriately Marked
-
-```lean broken
-axiom transform : Nat → Nat
-
-def transformIfZero : Nat → Nat
-  | 0 => transform 0
-  | n => n
-```
-```output
-`transform` not supported by code generator; consider marking definition as `noncomputable`
-```
-```lean fixed
-axiom transform : Nat → Nat
-
-noncomputable def transformIfZero : Nat → Nat
-  | 0 => transform 0
-  | n => n
-```
-In this example, `transformIfZero` depends on the axiom `transform`. Because `transform` is an
-axiom, it does not contain any executable code; although the value `transform 0` has type `Nat`,
-there is no way to compute its value. Thus, `transformIfZero` must be marked `noncomputable` because
-its execution would depend on this axiom.
-
-## Noncomputable Dependency Can Be Made Computable
-
-```lean broken
-noncomputable def getOrDefault [Nonempty α] : Option α → α
-  | some x => x
-  | none => Classical.ofNonempty
-
-def endsOrDefault (ns : List Nat) : Nat × Nat :=
-  let head := getOrDefault ns.head?
-  let tail := getOrDefault ns.getLast?
-  (head, tail)
-```
-```output
-failed to compile definition, consider marking it as 'noncomputable' because it depends on 'getOrDefault', which is 'noncomputable'
-```
-```lean fixed (title := "Fixed (computable)")
-def getOrDefault [Inhabited α] : Option α → α
-  | some x => x
-  | none => default
-
-def endsOrDefault (ns : List Nat) : Nat × Nat :=
-  let head := getOrDefault ns.head?
-  let tail := getOrDefault ns.getLast?
-  (head, tail)
-```
-The original definition of `getOrDefault` is noncomputable due to its use of `Classical.choice`.
-Unlike in the preceding example, however, it is possible to implement a similar but computable
-version of `getOrDefault` (using the `Inhabited` type class), allowing `endsOrDefault` to be
-computable. (The differences between `Inhabited` and `Nonempty` are described in the documentation
-of inhabited types in the manual section on [Basic Classes](lean-manual://section/basic-classes).)
-
-## Noncomputable Instance in Namespace
-
-```lean broken
-open Classical in
-/--
-Returns `y` if it is in the image of `f`,
-or an element of the image of `f` otherwise.
--/
-def fromImage (f : Nat → Nat) (y : Nat) :=
-  if ∃ x, f x = y then
-    y
-  else
-    f 0
-```
-```output
-failed to compile definition, consider marking it as 'noncomputable' because it depends on 'propDecidable', which is 'noncomputable'
-```
-```lean fixed
-open Classical in
-/--
-Returns `y` if it is in the image of `f`,
-or an element of the image of `f` otherwise.
--/
-noncomputable def fromImage (f : Nat → Nat) (y : Nat) :=
-  if ∃ x, f x = y then
-    y
-  else
-    f 0
-```
-The `Classical` namespace contains `Decidable` instances that are not computable. These are a common
-source of noncomputable dependencies that do not explicitly appear in the source code of a
-definition. In the above example, for instance, a `Decidable` instance for the proposition
-`∃ x, f x = y` is synthesized using a `Classical` decidability instance; therefore, `fromImage` must
-be marked `noncomputable`.
--/
-register_error_explanation lean.dependsOnNoncomputable {
-  summary := "Declaration depends on noncomputable definitions but is not marked as noncomputable"
-  sinceVersion := "4.22.0"
-}

src/Lean/ErrorExplanations/InductionWithNoAlts.lean

@@ -1,51 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Rob Simmons
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-/--
-Tactic-based proofs using induction in Lean need to use a pattern-matching-like notation to describe
-individual cases of the proof. However, the `induction'` tactic in Mathlib and the specialized
-`induction` tactic for natural numbers used in the Natural Number Game follows a different pattern.
-
-# Examples
-
-## Adding Explicit Cases to an Induction Proof
-
-```lean broken
-theorem zero_mul (m : Nat) : 0 * m = 0 := by
-  induction m with n n_ih
-  rw [Nat.mul_zero]
-  rw [Nat.mul_succ]
-  rw [Nat.add_zero]
-  rw [n_ih]
-```
-```output
-unknown tactic
-```
-```lean fixed
-theorem zero_mul (m : Nat) : 0 * m = 0 := by
-  induction m with
-  | zero =>
-    rw [Nat.mul_zero]
-  | succ n n_ih =>
-    rw [Nat.mul_succ]
-    rw [Nat.add_zero]
-    rw [n_ih]
-```
-The broken example has the structure of a correct proof in the Natural Numbers Game, and this
-proof will work if you `import Mathlib` and replace `induction` with `induction'`. Induction tactics
-in basic Lean expect the `with` keyword to be followed by a series of cases, and the names for
-the inductive case are provided in the `succ` case rather than being provided up-front.
-
--/
-register_error_explanation lean.inductionWithNoAlts {
-  summary := "Induction pattern with nontactic in natural-number-game-style `with` clause."
-  sinceVersion := "4.26.0"
-}

src/Lean/ErrorExplanations/InductiveParamMismatch.lean

@@ -1,62 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error occurs when a parameter of an inductive type is not uniform in an inductive
-declaration. The parameters of an inductive type (i.e., those that appear before the colon following
-the `inductive` keyword) must be identical in all occurrences of the type being defined in its
-constructors' types. If a parameter of an inductive type must vary between constructors, make the
-parameter an index by moving it to the right of the colon. See the manual section on
-[Inductive Types](lean-manual://section/inductive-types) for additional details.
-
-Note that auto-implicit inlay hints always appear left of the colon in an inductive declaration
-(i.e., as parameters), even when they are actually indices. This means that double-clicking on an
-inlay hint to insert such parameters may result in this error. If it does, change the inserted
-parameters to indices.
-
-# Examples
-
-## Vector Length Index as a Parameter
-
-```lean broken
-inductive Vec (α : Type) (n : Nat) : Type where
-  | nil  : Vec α 0
-  | cons : α → Vec α n → Vec α (n + 1)
-```
-```output broken
-Mismatched inductive type parameter in
-  Vec α 0
-The provided argument
-  0
-is not definitionally equal to the expected parameter
-  n
-
-Note: The value of parameter `n` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.
-```
-```lean fixed
-inductive Vec (α : Type) : Nat → Type where
-  | nil  : Vec α 0
-  | cons : α → Vec α n → Vec α (n + 1)
-```
-
-The length argument `n` of the `Vec` type constructor is declared as a parameter, but other values
-for this argument appear in the `nil` and `cons` constructors (namely, `0` and `n + 1`). An error
-therefore appears at the first occurrence of such an argument. To correct this, `n` cannot be a
-parameter of the inductive declaration and must instead be an index, as in the corrected example. On
-the other hand, `α` remains unchanged throughout all occurrences of `Vec` in the declaration and so
-is a valid parameter.
--/
-register_error_explanation lean.inductiveParamMismatch {
-  summary := "Invalid parameter in an occurrence of an inductive type in one of its constructors."
-  sinceVersion := "4.22.0"
-}

src/Lean/ErrorExplanations/InductiveParamMissing.lean

@@ -1,71 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error occurs when an inductive type constructor is partially applied in the type of one of its
-constructors such that one or more parameters of the type are omitted. The elaborator requires that
-all parameters of an inductive type be specified everywhere that type is referenced in its
-definition, including in the types of its constructors.
-
-If it is necessary to allow the type constructor to be partially applied, without specifying a given
-type parameter, that parameter must be converted to an index. See the manual section on
-[Inductive Types](lean-manual://section/inductive-types) for further explanation of the difference
-between indices and parameters.
-
-# Examples
-
-## Omitting Parameter in Argument to Higher-Order Predicate
-
-```lean broken
-inductive List.All {α : Type u} (P : α → Prop) : List α → Prop
-  | nil : All P []
-  | cons {x xs} : P x → All P xs → All P (x :: xs)
-
-structure RoseTree (α : Type u) where
-  val : α
-  children : List (RoseTree α)
-
-inductive RoseTree.All {α : Type u} (P : α → Prop) (t : RoseTree α) : Prop
-  | intro : P t.val → List.All (All P) t.children → All P t
-```
-```output
-Missing parameter(s) in occurrence of inductive type: In the expression
-  List.All (All P) t.children
-found
-  All P
-but expected all parameters to be specified:
-  All P t
-
-Note: All occurrences of an inductive type in the types of its constructors must specify its fixed parameters. Only indices can be omitted in a partial application of the type constructor.
-```
-```lean fixed
-inductive List.All {α : Type u} (P : α → Prop) : List α → Prop
-  | nil : All P []
-  | cons {x xs} : P x → All P xs → All P (x :: xs)
-
-structure RoseTree (α : Type u) where
-  val : α
-  children : List (RoseTree α)
-
-inductive RoseTree.All {α : Type u} (P : α → Prop) : RoseTree α → Prop
-  | intro : P t.val → List.All (All P) t.children → All P t
-```
-Because the `RoseTree.All` type constructor must be partially applied in the argument to `List.All`,
-the unspecified argument (`t`) must not be a parameter of the `RoseTree.All` predicate. Making it an
-index to the right of the colon in the header of `RoseTree.All` allows this partial application to
-succeed.
--/
-register_error_explanation lean.inductiveParamMissing {
-  summary := "Parameter not present in an occurrence of an inductive type in one of its constructors."
-  sinceVersion := "4.22.0"
-}

src/Lean/ErrorExplanations/InferBinderTypeFailed.lean

@@ -1,164 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error occurs when the type of a binder in a declaration header or local binding is not fully
-specified and cannot be inferred by Lean. Generally, this can be resolved by providing more
-information to help Lean determine the type of the binder, either by explicitly annotating its type
-or by providing additional type information at sites where it is used. When the binder in question
-occurs in the header of a declaration, this error is often accompanied by
-[`lean.inferDefTypeFailed`](lean-manual://errorExplanation/lean.inferDefTypeFailed).
-
-Note that if a declaration is annotated with an explicit resulting type—even one that contains
-holes—Lean will not use information from the definition body to infer parameter types. It may
-therefore be necessary to explicitly specify the types of parameters whose types would otherwise be
-inferable without the resulting-type annotation; see the "uninferred binder due to resulting type
-annotation" example below for a demonstration. In `theorem` declarations, the body is never used to
-infer the types of binders, so any binders whose types cannot be inferred from the rest of the
-theorem type must include a type annotation.
-
-This error may also arise when identifiers that were intended to be declaration names are
-inadvertently written in binder position instead. In these cases, the erroneous identifiers are
-treated as binders with unspecified type, leading to a type inference failure. This frequently
-occurs when attempting to simultaneously define multiple constants of the same type using syntax
-that does not support this. Such situations include:
-* Attempting to name an example by writing an identifier after the `example` keyword;
-* Attempting to define multiple constants with the same type and (if applicable) value by listing
-  them sequentially after `def`, `opaque`, or another declaration keyword;
-* Attempting to define multiple fields of a structure of the same type by sequentially listing their
-  names on the same line of a structure declaration; and
-* Omitting vertical bars between inductive constructor names.
-
-The first three cases are demonstrated in examples below.
-
-# Examples
-
-## Binder Type Requires New Type Variable
-
-```lean broken
-def identity x :=
-  x
-```
-```output
-Failed to infer type of binder `x`
-```
-```lean fixed
-def identity (x : α) :=
-  x
-```
-
-In the code above, the type of `x` is unconstrained; as this example demonstrates, Lean does not
-automatically generate fresh type variables for such binders. Instead, the type `α` of `x` must be
-specified explicitly. Note that if automatic implicit parameter insertion is enabled (as it is by
-default), a binder for `α` itself need not be provided; Lean will insert an implicit binder for this
-parameter automatically.
-
-## Uninferred Binder Type Due to Resulting Type Annotation
-
-```lean broken
-def plusTwo x : Nat :=
-  x + 2
-```
-```output
-Failed to infer type of binder `x`
-
-Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be
-```
-```lean fixed
-def plusTwo (x : Nat) : Nat :=
-  x + 2
-```
-
-Even though `x` is inferred to have type `Nat` in the body of `plusTwo`, this information is not
-available when elaborating the type of the definition because its resulting type (`Nat`) has been
-explicitly specified. Considering only the information in the header, the type of `x` cannot be
-determined, resulting in the shown error. It is therefore necessary to include the type of `x` in
-its binder.
-
-
-## Attempting to Name an Example Declaration
-
-```lean broken
-example trivial_proof : True :=
-  trivial
-```
-```output
-Failed to infer type of binder `trivial_proof`
-
-Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be
-```
-```lean fixed
-example : True :=
-  trivial
-```
-This code is invalid because it attempts to give a name to an `example` declaration. Examples cannot
-be named, and an identifier written where a name would appear in other declaration forms is instead
-elaborated as a binder, whose type cannot be inferred. If a declaration must be named, it should be
-defined using a declaration form that supports naming, such as `def` or `theorem`.
-
-## Attempting to Define Multiple Opaque Constants at Once
-
-```lean broken
-opaque m n : Nat
-```
-```output
-Failed to infer type of binder `n`
-
-Note: Multiple constants cannot be declared in a single declaration. The identifier(s) `n` are being interpreted as parameters `(n : _)`.
-```
-```lean fixed
-opaque m : Nat
-opaque n : Nat
-```
-
-This example incorrectly attempts to define multiple constants with a single `opaque` declaration.
-Such a declaration can define only one constant: it is not possible to list multiple identifiers
-after `opaque` or `def` to define them all to have the same type (or value). Such a declaration is
-instead elaborated as defining a single constant (e.g., `m` above) with parameters given by the
-subsequent identifiers (`n`), whose types are unspecified and cannot be inferred. To define multiple
-global constants, it is necessary to declare each separately.
-
-## Attempting to Define Multiple Structure Fields on the Same Line
-
-```lean broken
-structure Person where
-  givenName familyName : String
-  age : Nat
-```
-```output
-Failed to infer type of binder `familyName`
-```
-```lean fixed (title := "Fixed (separate lines)")
-structure Person where
-  givenName : String
-  familyName : String
-  age : Nat
-```
-```lean fixed (title := "Fixed (parenthesized)")
-structure Person where
-  (givenName familyName : String)
-  age : Nat
-```
-
-This example incorrectly attempts to define multiple structure fields (`givenName` and `familyName`)
-of the same type by listing them consecutively on the same line. Lean instead interprets this as
-defining a single field, `givenName`, parametrized by a binder `familyName` with no specified type.
-The intended behavior can be achieved by either listing each field on a separate line, or enclosing
-the line specifying multiple field names in parentheses (see the manual section on
-[Inductive Types](lean-manual://section/inductive-types) for further details about structure
-declarations).
--/
-register_error_explanation lean.inferBinderTypeFailed {
-  summary := "The type of a binder could not be inferred."
-  sinceVersion := "4.23.0"
-}

src/Lean/ErrorExplanations/InferDefTypeFailed.lean

@@ -1,87 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error occurs when the type of a definition is not fully specified and Lean is unable to infer
-its type from the available information. If the definition has parameters, this error refers only to
-the resulting type after the colon (the error
-[`lean.inferBinderTypeFailed`](lean-manual://errorExplanation/lean.inferBinderTypeFailed) indicates
-that a parameter type could not be inferred).
-
-To resolve this error, provide additional type information in the definition. This can be done
-straightforwardly by providing an explicit resulting type after the colon in the definition
-header. Alternatively, if an explicit resulting type is not provided, adding further type
-information to the definition's body—such as by specifying implicit type arguments or giving
-explicit types to `let` binders—may allow Lean to infer the type of the definition. Look for type
-inference or implicit argument synthesis errors that arise alongside this one to identify
-ambiguities that may be contributing to this error.
-
-Note that when an explicit resulting type is provided—even if that type contains holes—Lean will not
-use information from the definition body to help infer the type of the definition or its parameters.
-Thus, adding an explicit resulting type may also necessitate adding type annotations to parameters
-whose types were previously inferrable. Additionally, it is always necessary to provide an explicit
-type in a `theorem` declaration: the `theorem` syntax requires a type annotation, and the elaborator
-will never attempt to use the theorem body to infer the proposition being proved.
-
-# Examples
-
-## Implicit Argument Cannot be Inferred
-
-```lean broken
-def emptyNats :=
-  []
-```
-```output
-Failed to infer type of definition `emptyNats`
-```
-
-```lean fixed (title := "Fixed (type annotation)")
-def emptyNats : List Nat :=
-  []
-```
-```lean fixed (title := "Fixed (implicit argument)")
-def emptyNats :=
-  List.nil (α := Nat)
-```
-
-Here, Lean is unable to infer the value of the parameter `α` of the `List` type constructor, which
-in turn prevents it from inferring the type of the definition. Two fixes are possible: specifying
-the expected type of the definition allows Lean to infer the appropriate implicit argument to the
-`List.nil` constructor; alternatively, making this implicit argument explicit in the function body
-provides sufficient information for Lean to infer the definition's type.
-
-## Definition Type Uninferrable Due to Unknown Parameter Type
-
-```lean broken
-def identity x :=
-  x
-```
-```output
-Failed to infer type of definition `identity`
-```
-```lean fixed
-def identity (x : α) :=
-  x
-```
-
-In this example, the type of `identity` is determined by the type of `x`, which cannot be inferred.
-Both the indicated error and
-[lean.inferBinderTypeFailed](lean-manual://errorExplanation/lean.inferBinderTypeFailed) therefore
-appear (see that explanation for additional discussion of this example). Resolving the latter—by
-explicitly specifying the type of `x`—provides Lean with sufficient information to infer the
-definition type.
--/
-register_error_explanation lean.inferDefTypeFailed {
-  summary := "The type of a definition could not be inferred."
-  sinceVersion := "4.23.0"
-}

src/Lean/ErrorExplanations/InvalidDottedIdent.lean

@@ -1,78 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error indicates that dotted identifier notation was used in an invalid or unsupported context.
-Dotted identifier notation allows an identifier's namespace to be omitted, provided that it can be
-inferred by Lean based on type information. Details about this notation can be found in the manual
-section on [identifiers](lean-manual://section/identifiers-and-resolution).
-
-This notation can only be used in a term whose type Lean is able to infer. If there is insufficient
-type information for Lean to do so, this error will be raised. The inferred type must not be a type
-universe (e.g., `Prop` or `Type`), as dotted-identifier notation is not supported on these types.
-
-# Examples
-
-## Insufficient Type Information
-
-```lean broken
-def reverseDuplicate (xs : List α) :=
-  .reverse (xs ++ xs)
-```
-```output
-Invalid dotted identifier notation: The expected type of `.reverse` could not be determined
-```
-```lean fixed
-def reverseDuplicate (xs : List α) : List α :=
-  .reverse (xs ++ xs)
-```
-Because the return type of `reverseDuplicate` is not specified, the expected type of `.reverse`
-cannot be determined. Lean will not use the type of the argument `xs ++ xs` to infer the omitted
-namespace. Adding the return type `List α` allows Lean to infer the type of `.reverse` and thus the
-appropriate namespace (`List`) in which to resolve this identifier.
-
-Note that this means that changing the return type of `reverseDuplicate` changes how `.reverse`
-resolves: if the return type is  `T`, then Lean will (attempt to) resolve `.reverse` to a function
-`T.reverse` whose return type is `T`—even if `T.reverse` does not take an argument of type
-`List α`.
-
-## Dotted Identifier Where Type Universe Expected
-
-```lean broken
-example (n : Nat) :=
-  match n > 42 with
-  | .true  => n - 1
-  | .false => n + 1
-```
-```output
-Invalid dotted identifier notation: Not supported on type universe
-  Prop
-```
-```lean fixed
-example (n : Nat) :=
-  match decide (n > 42) with
-  | .true  => n - 1
-  | .false => n + 1
-```
-
-The proposition `n > 42` has type `Prop`, which, being a type universe, does not support
-dotted-identifier notation. As this example demonstrates, attempting to use this notation in such a
-context is almost always an error. The intent in this example was for `.true` and `.false` to be
-Booleans, not propositions; however, `match` expressions do not automatically perform this coercion
-for decidable propositions. Explicitly adding `decide` makes the discriminant a `Bool` and allows
-the dotted-identifier resolution to succeed.
--/
-register_error_explanation lean.invalidDottedIdent {
-  summary := "Dotted identifier notation used with invalid or uninferrable expected type."
-  sinceVersion := "4.22.0"
-}

src/Lean/ErrorExplanations/InvalidField.lean

@@ -1,99 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Rob Simmons
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-/--
-This error indicates that an expression containing a dot followed by an identifier was encountered,
-and that it wasn't possible to understand the identifier as a field.
-
-Lean's field notation is very powerful, but this can also make it confusing: the expression
-`color.value` can either be a single [identifier](lean-manual://section/identifiers-and-resolution),
-it can be a reference to the [field of a structure](lean-manual://section/structure-fields), and it
-and be a calling a function on the value `color` with
-[generalized field notation](lean-manual://section/generalized-field-notation).
-
-# Examples
-
-## Incorrect Field Name
-
-```lean broken
-#eval (4 + 2).suc
-```
-```output
-Invalid field `suc`: The environment does not contain `Nat.suc`, so it is not possible to project the field `suc` from an expression
-  4 + 2
-of type `Nat`
-```
-```lean fixed
-#eval (4 + 1).succ
-```
-
-The simplest reason for an invalid field error is that the function being sought, like `Nat.suc`,
-does not exist.
-
-## Projecting from the Wrong Expression
-
-```lean broken
-#eval '>'.leftpad 10 ['a', 'b', 'c']
-```
-```output
-Invalid field `leftpad`: The environment does not contain `Char.leftpad`, so it is not possible to project the field `leftpad` from an expression
-  '>'
-of type `Char`
-```
-```lean fixed
-#eval ['a', 'b', 'c'].leftpad 10 '>'
-```
-
-The type of the expression before the dot entirely determines the function being called by the field
-projection. There is no `Char.leftpad`, and the only way to invoke `List.leftpad` with generalized
-field notation is to have the list come before the dot.
-
-## Type is Not Specific
-
-```lean broken
-def double_plus_one {α} [Add α] (x : α) :=
-   (x + x).succ
-```
-```output
-Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
-  x + x
-has type `α` which does not have the necessary form.
-```
-```lean fixed
-def double_plus_one (x : Nat) :=
-   (x + x).succ
-```
-
-The `Add` typeclass is sufficient for performing the addition `x + x`, but the `.succ` field notation
-cannot operate without knowing more about the actual type from which `succ` is being projected.
-
-## Insufficient Type Information
-
-```lean broken
-example := fun (n) => n.succ.succ
-```
-```output
-Invalid field notation: Type of
-  n
-is not known; cannot resolve field `succ`
-```
-```lean fixed
-example := fun (n : Nat) => n.succ.succ
-```
-
-Generalized field notation can only be used when it is possible to determine the type that is being
-projected. Type annotations may need to be added to make generalized field notation work.
-
--/
-register_error_explanation lean.invalidField {
-  summary := "Dotted identifier notation used without ."
-  sinceVersion := "4.22.0"
-}

src/Lean/ErrorExplanations/ProjNonPropFromProp.lean

@@ -1,62 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error occurs when attempting to project a piece of data from a proof of a proposition using an
-index projection. For example, if `h` is a proof of an existential proposition, attempting to
-extract the witness `h.1` is an example of this error. Such projections are disallowed because they
-may violate Lean's prohibition of large elimination from `Prop` (refer to the
-[Propositions](lean-manual://section/propositions) manual section for further details).
-
-Instead of an index projection, consider using a pattern-matching `let`, `match` expression, or a
-destructuring tactic like `cases` to eliminate from one propositional type to another. Note that
-such elimination is only valid if the resulting value is also in `Prop`; if it is not, the error
-[`lean.propRecLargeElim`](lean-manual://errorExplanation/lean.propRecLargeElim) will be raised.
-
-# Examples
-
-## Attempting to Use Index Projection on Existential Proof
-
-```lean broken
-example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > 0 :=
-  ⟨h.1, Nat.lt_of_succ_lt h.2⟩
-```
-```output
-Invalid projection: Cannot project a value of non-propositional type
-  Nat
-from the expression
-  h
-which has propositional type
-  ∃ x, x > a + 1
-```
-```lean fixed (title := "Fixed (let)")
-example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > a :=
-  let ⟨w, hw⟩ := h
-  ⟨w, Nat.lt_of_succ_lt hw⟩
-```
-```lean (title := "Fixed (cases)")
-example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > a := by
-  cases h with
-  | intro w hw =>
-    exists w
-    omega
-```
-
-The witness associated with a proof of an existential proposition cannot be extracted using an
-index projection. Instead, it is necessary to use a pattern match: either a term like a `let`
-binding or a tactic like `cases`.
--/
-register_error_explanation lean.projNonPropFromProp {
-  summary := "Tried to project data from a proof."
-  sinceVersion := "4.23.0"
-}

src/Lean/ErrorExplanations/PropRecLargeElim.lean

@@ -1,131 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error occurs when attempting to eliminate a proof of a proposition into a higher type universe.
-Because Lean's type theory does not allow large elimination from `Prop`, it is invalid to
-pattern-match on such values—e.g., by using `let` or `match`—to produce a piece of data in a
-non-propositional universe (i.e., `Type u`). More precisely, the motive of a propositional recursor
-must be a proposition. (See the manual section on
-[Subsingleton Elimination](lean-manual://section/subsingleton-elimination) for exceptions to this
-rule.)
-
-Note that this error will arise in any expression that eliminates from a proof into a
-non-propositional universe, even if that expression occurs within another expression of
-propositional type (e.g., in a `let` binding in a proof). The "Defining an intermediate data value
-within a proof" example below demonstrates such an occurrence. Errors of this kind can usually be
-resolved by moving the recursor application "outward," so that its motive is the proposition being
-proved rather than the type of data-valued term.
-
-# Examples
-
-## Defining an Intermediate Data Value Within a Proof
-
-```lean broken
-example {α : Type} [inst : Nonempty α] (p : α → Prop) :
-    ∃ x, p x ∨ ¬ p x :=
-  let val :=
-    match inst with
-    | .intro x => x
-  ⟨val, Classical.em (p val)⟩
-```
-```output
-Tactic `cases` failed with a nested error:
-Tactic `induction` failed: recursor `Nonempty.casesOn` can only eliminate into `Prop`
-
-α : Type
-motive : Nonempty α → Sort ?u.48
-h_1 : (x : α) → motive ⋯
-inst✝ : Nonempty α
-⊢ motive inst✝
- after processing
-  _
-the dependent pattern matcher can solve the following kinds of equations
-- <var> = <term> and <term> = <var>
-- <term> = <term> where the terms are definitionally equal
-- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
-```
-```lean fixed
-example {α : Type} [inst : Nonempty α] (p : α → Prop) :
-    ∃ x, p x ∨ ¬ p x :=
-  match inst with
-  | .intro x => ⟨x, Classical.em (p x)⟩
-```
-Even though the `example` being defined has a propositional type, the body of `val` does not; it has
-type `α : Type`. Thus, pattern-matching on the proof of `Nonempty α` (a proposition) to produce
-`val` requires eliminating that proof into a non-propositional type and is disallowed. Instead, the
-`match` expression must be moved to the top level of the `example`, where the result is a
-`Prop`-valued proof of the existential claim stated in the example's header. This restructuring
-could also be done using a pattern-matching `let` binding.
-
-## Extracting the Witness from an Existential Proof
-
-```lean broken
-def getWitness {α : Type u} {p : α → Prop} (h : ∃ x, p x) : α :=
-  match h with
-  | .intro x _ => x
-```
-```output
-Tactic `cases` failed with a nested error:
-Tactic `induction` failed: recursor `Exists.casesOn` can only eliminate into `Prop`
-
-α : Type u
-p : α → Prop
-motive : (∃ x, p x) → Sort ?u.52
-h_1 : (x : α) → (h : p x) → motive ⋯
-h✝ : ∃ x, p x
-⊢ motive h✝
- after processing
-  _
-the dependent pattern matcher can solve the following kinds of equations
-- <var> = <term> and <term> = <var>
-- <term> = <term> where the terms are definitionally equal
-- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
-```
-```lean fixed (title := "Fixed (in Prop)")
--- This is `Exists.elim`
-theorem useWitness {α : Type u} {p : α → Prop} {q : Prop}
-    (h : ∃ x, p x) (hq : (x : α) → p x → q) : q :=
-  match h with
-  | .intro x hx => hq x hx
-```
-```lean fixed (title := "Fixed (in Type)")
-def getWitness {α : Type u} {p : α → Prop}
-    (h : (x : α) ×' p x) : α :=
-  match h with
-  | .mk x _ => x
-```
-In this example, simply relocating the pattern-match is insufficient; the attempted definition
-`getWitness` is fundamentally unsound. (Consider the case where `p` is `fun (n : Nat) => n > 0`: if
-`h` and `h'` are proofs of `∃ x, x > 0`, with `h` using witness `1` and `h'` witness `2`, then since
-`h = h'` by proof irrelevance, it follows that `getWitness h = getWitness h'`—i.e., `1 = 2`.)
-
-Instead, `getWitness` must be rewritten: either the resulting type of the function must be a
-proposition (the first fixed example above), or `h` must not be a proposition (the second).
-
-In the first corrected example, the resulting type of `useWitness` is now a proposition `q`. This
-allows us to pattern-match on `h`—since we are eliminating into a propositional type—and pass the
-unpacked values to `hq`. From a programmatic perspective, one can view `useWitness` as rewriting
-`getWitness` in continuation-passing style, restricting subsequent computations to use its result
-only to construct values in `Prop`, as required by the prohibition on propositional large
-elimination. Note that `useWitness` is the existential elimination principle `Exists.elim`.
-
-The second corrected example changes the type of `h` from an existential proposition to a
-`Type`-valued dependent pair (corresponding to the `PSigma` type constructor). Since this type is
-not propositional, eliminating into `α : Type u` is no longer invalid, and the previously attempted
-pattern match now type-checks.
--/
-register_error_explanation lean.propRecLargeElim {
-  summary := "Attempted to eliminate a proof into a higher type universe."
-  sinceVersion := "4.23.0"
-}

src/Lean/ErrorExplanations/README.md

@@ -1,95 +0,0 @@
-# Error Explanations
-
-## Overview
-
-This directory contains explanations for named errors in Lean core.
-Explanations associate to each named error or warning a long-form
-description of its meaning and causes, relevant background
-information, and strategies for correcting erroneous code. They also
-provide examples of incorrect and corrected code. While error
-explanations are declared in source, they are viewed as part of
-external documentation linked from error messages.
-
-Explanations straddle the line between diagnostics and documentation:
-unlike the error messages they describe, explanations serve not only
-to aid the debugging process but also to help users understand the
-principles of the language that underlie the error. Accordingly, error
-explanations should be written with both of these aims in mind. Refer
-to existing explanations for examples of the formatting and content
-conventions described here.
-
-Once an error explanation has been registered, use the macros
-`throwNamedError`, `logNamedError`, `throwNamedErrorAt` and
-`logNamedErrorAt` to tag error messages with the appropriate
-explanation name. Doing so will display a widget in the Infoview with
-the name of the error and a link to the corresponding explanation.
-
-## Registering Explanations
-
-New error explanations are declared using the
-`register_error_explanation` command. Each explanation should
-appear in a separate submodule of `Lean.ErrorExplanations` whose name
-matches the error name being declared; the module should be marked
-with `prelude` and import only `Lean.ErrorExplanation`. The
-`register_error_explanation` keyword is preceded by a doc
-comment containing the explanation (written in Markdown, following the
-structure guidelines below) and is followed by the name of the
-explanation and a `Lean.ErrorExplanation.Metadata` structure
-describing the error. All errors have two-component names: the first
-identifies the package or "domain" to which the error belongs (in
-core, this will nearly always be `lean`); the second identifies the
-error itself. Error names are written in upper camel case and should
-be descriptive but not excessively verbose. Abbreviations in error
-names are acceptable, but they should be reasonably clear (e.g.,
-abbreviations that are commonly used elsewhere in Lean, such as `Ctor`
-for "constructor") and should not be ambiguous with other vocabulary
-likely to appear in error names (e.g., use `Indep` rather than `Ind`
-for "independent," since the latter could be confused with
-"inductive").
-
-
-## Structure
-
-### Descriptions
-
-Error explanations consist of two parts: a prose description of the
-error and code examples. The description should begin by explaining
-the meaning of the error and why it occurs. It should also briefly
-explain, if appropriate, any relevant context, such as related errors
-or relevant entries in the reference manual. The latter is especially
-useful for directing users to important concepts for understanding an
-error: while it is appropriate to provide brief conceptual exposition
-in an error explanation, avoid extensively duplicating content that
-can be found elsewhere in the manual. General resolution or debugging
-strategies not tied to specific examples can also be discussed in the
-description portion of an explanation.
-
-### Examples
-
-The second half of an explanation (set off by the level-1 header
-"Examples") contains annotated code examples. Each of these consists
-of a level-2 header with the name of the example, followed immediately
-by a sequence of code blocks containing self-contained minimal working
-(or error-producing) examples (MWEs) and outputs. The first MWE should
-have the Markdown info string `lean broken` and demonstrate the error
-in question; it should be followed by an `output` code block with the
-corresponding error message. Subsequent MWEs should have the info
-string `lean fixed` and illustrate how to rewrite the code correctly.
-Finally, after these MWEs, include explanatory text describing the
-example and the cause and resolution of the error it demonstrates.
-
-Note that each MWE in an example will be rendered as a tab, and the
-full example (including its explanatory text) will appear in a
-collapsible "Example" block like those used elsewhere in the manual.
-Include `(title := "Title")` in the info string of an MWE to assign it
-a custom title (for instance, if there are multiple "fixed" MWEs).
-Examples should center on code: prose not specific to the example
-should generally appear in the initial half of the explanation.
-However, an example should provide sufficient commentary for users to
-understand how it illustrates relevant ideas from the preceding
-description and what was done to resolve the exemplified error.
-
-Choose examples carefully: they should be relatively minimal, so as to
-draw out the error itself, but not so contrived as to impede
-comprehension. Each should contain a distinct, representative instance
-of the error to avoid the need for excessively many.

src/Lean/ErrorExplanations/RedundantMatchAlt.lean

@@ -1,120 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error occurs when an alternative in a pattern match can never be reached: any values that would
-match the provided patterns would also match some preceding alternative. Refer to the
-[Pattern Matching](lean-manual://section/pattern-matching) manual section for additional details
-about pattern matching.
-
-This error may appear in any pattern matching expression, including `match` expressions, equational
-function definitions, `if let` bindings, and monadic `let` bindings with fallback clauses.
-
-In pattern-matches with multiple arms, this error may occur if a less-specific pattern precedes a
-more-specific one that it subsumes. Bear in mind that expressions are matched against patterns from
-top to bottom, so specific patterns should precede generic ones.
-
-In `if let` bindings and monadic `let` bindings with fallback clauses, in which only one pattern is
-specified, this error indicates that the specified pattern will always be matched. In this case, the
-binding in question can be replaced with a standard pattern-matching `let`.
-
-One common cause of this error is that a pattern that was intended to match a constructor was
-instead interpreted as a variable binding. This occurs, for instance, if a constructor
-name (e.g., `cons`) is written without its prefix (`List`) outside of that type's namespace. The
-constructor-name-as-variable linter, enabled by default, will display a warning on any variable
-patterns that resemble constructor names.
-
-This error nearly always indicates an issue with the code where it appears. If needed, however,
-`set_option match.ignoreUnusedAlts true` will disable the check for this error and allow pattern
-matches with redundant alternatives to be compiled by discarding the unused arms.
-
-# Examples
-
-## Incorrect Ordering of Pattern Matches
-
-```lean broken
-def seconds : List (List α) → List α
-  | [] => []
-  | _ :: xss => seconds xss
-  | (_ :: x :: _) :: xss => x :: seconds xss
-```
-```output
-Redundant alternative: Any expression matching
-  (head✝ :: x :: tail✝) :: xss
-will match one of the preceding alternatives
-```
-```lean fixed
-def seconds : List (List α) → List α
-  | [] => []
-  | (_ :: x :: _) :: xss => x :: seconds xss
-  | _ :: xss => seconds xss
-```
-
-Since any expression matching `(_ :: x :: _) :: xss` will also match `_ :: xss`, the last
-alternative in the broken implementation is never reached. We resolve this by moving the more
-specific alternative before the more general one.
-
-## Unnecessary Fallback Clause
-
-```lean broken
-example (p : Nat × Nat) : IO Nat := do
-  let (m, n) := p
-    | return 0
-  return m + n
-```
-```output
-Redundant alternative: Any expression matching
-  x✝
-will match one of the preceding alternatives
-```
-```lean fixed
-example (p : Nat × Nat) : IO Nat := do
-  let (m, n) := p
-  return m + n
-```
-
-Here, the fallback clause serves as a catch-all for all values of `p` that do not match `(m, n)`.
-However, no such values exist, so the fallback clause is unnecessary and can be removed. A similar
-error arises when using `if let pat := e` when `e` will always match `pat`.
-
-## Pattern Treated as Variable, Not Constructor
-
-```lean broken
-example (xs : List Nat) : Bool :=
-  match xs with
-  | nil => false
-  | _ => true
-```
-```output
-Redundant alternative: Any expression matching
-  x✝
-will match one of the preceding alternatives
-```
-```lean fixed
-example (xs : List Nat) : Bool :=
-  match xs with
-  | .nil => false
-  | _ => true
-```
-
-In the original example, `nil` is treated as a variable, not as a constructor name, since this
-definition is not within the `List` namespace. Thus, all values of `xs` will match the first
-pattern, rendering the second unused. Notice that the constructor-name-as-variable linter displays a
-warning at `nil`, indicating its similarity to a valid constructor name. Using dot-prefix notation,
-as shown in the fixed example, or specifying the full constructor name `List.nil` achieves the
-intended behavior.
--/
-register_error_explanation lean.redundantMatchAlt {
-  summary := "Match alternative will never be reached."
-  sinceVersion := "4.22.0"
-}

src/Lean/ErrorExplanations/SynthInstanceFailed.lean

@@ -1,125 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Rob Simmons
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-[Type classes](lean-manual://section/type-class) are the mechanism that Lean and many other
-programming languages use to handle overloaded operations. The code that handles a particular
-overloaded operation is an _instance_ of a typeclass; deciding which instance to use for a given
-overloaded operation is called _synthesizing_ an instance.
-
-As an example, when Lean encounters an expression `x + y` where `x` and `y` both have type `Int`,
-it is necessary to look up how it should add two integers and also look up what the resulting type
-will be. This is described as synthesizing an instance of the type class `HAdd Int Int t` for some
-type `t`.
-
-Many failures to synthesize an instance of a type class are the result of using the wrong binary
-operation. Both success and failure are not always straightforward, because some instances are
-defined in terms of other instances, and Lean must recursively search to find appropriate instances.
-It's possible to inspect Lean's instance synthesis](lean-manual://section/instance-search), and this
-can be helpful for diagnosing tricky failures of type class instance synthesis.
-
-# Examples
-
-## Using the Wrong Binary Operation
-
-```lean broken
-#eval "A" + "3"
-```
-```output
-failed to synthesize instance of type class
-  HAdd String String ?m.4
-
-Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-```
-```lean fixed
-#eval "A" ++ "3"
-```
-
-The binary operation `+` is associated with the `HAdd` type class, and there's no way to add two
-strings. The binary operation `++`, associated with the `HAppend` type class, is the correct way to
-append strings.
-
-## Arguments Have the Wrong Type
-
-```lean broken
-def x : Int := 3
-#eval x ++ "meters"
-```
-```output
-failed to synthesize instance of type class
-  HAppend Int String ?m.4
-
-Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-```
-```lean fixed
-def x : Int := 3
-#eval ToString.toString x ++ "meters"
-```
-
-Lean does not allow integers and strings to be added directly. The function `ToString.toString` uses
-type class overloading to convert values to strings; by successfully searching for an instance of
-`ToString Int`, the second example will succeed.
-
-## Missing Type Class Instance
-
-```lean broken
-inductive MyColor where
-  | chartreuse | sienna | thistle
-
-def forceColor (oc : Option MyColor) :=
-  oc.get!
-```
-```output
-failed to synthesize instance of type class
-  Inhabited MyColor
-
-Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-```
-```lean fixed (title := "Fixed (derive instance when defining type)")
-inductive MyColor where
-  | chartreuse | sienna | thistle
-deriving Inhabited
-
-def forceColor (oc : Option MyColor) :=
-  oc.get!
-```
-```lean fixed (title := "Fixed (derive instance separately)")
-inductive MyColor where
-  | chartreuse | sienna | thistle
-
-deriving instance Inhabited for MyColor
-
-def forceColor (oc : Option MyColor) :=
-  oc.get!
-```
-```lean fixed (title := "Fixed (define instance)")
-inductive MyColor where
-  | chartreuse | sienna | thistle
-
-instance : Inhabited MyColor where
-  default := .sienna
-
-def forceColor (oc : Option MyColor) :=
-  oc.get!
-```
-
-Type class synthesis can fail because an instance of the type class simply needs to be provided.
-This commonly happens for type classes like `Repr`, `BEq`, `ToJson` and `Inhabited`. Lean can often
-[automatically generate instances of the type class with the `deriving` keyword](lean-manual://section/type-class),
-either when the type is defined or with the stand-alone `deriving` command.
-
--/
-register_error_explanation lean.synthInstanceFailed {
-  summary := "Failed to synthesize instance of type class"
-  sinceVersion := "4.26.0"
-}

src/Lean/ErrorExplanations/UnknownIdentifier.lean

@@ -1,236 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-/--
-This error means that Lean was unable to find a variable or constant matching the given name. More
-precisely, this means that the name could not be *resolved*, as described in the manual section on
-[Identifiers](lean-manual://section/identifiers-and-resolution): no interpretation of the input as
-the name of a local or section variable (if applicable), a previously declared global constant, or a
-projection of either of the preceding was valid. ("If applicable" refers to the fact that in some
-cases—e.g., the `#print` command's argument—names are resolved only to global constants.)
-
-Note that this error message will display only one possible resolution of the identifier, but the
-presence of this error indicates failures for *all* possible names to which it might refer. For
-example, if the identifier `x` is entered with the namespaces `A` and `B` are open, the error
-message "Unknown identifier \`x\`" indicates that none of `x`, `A.x`, or `B.x` could be found (or
-that `A.x` or `B.x`, if either exists, is a protected declaration).
-
-Common causes of this error include forgetting to import the module in which a constant is defined,
-omitting a constant's namespace when that namespace is not open, or attempting to refer to a local
-variable that is not in scope.
-
-To help resolve some of these common issues, this error message is accompanied by a code action that
-suggests constant names similar to the one provided. These include constants in the environment as
-well as those that can be imported from other modules. Note that these suggestions are available
-only through supported code editors' built-in code action mechanisms and not as a hint in the error
-message itself.
-
-# Examples
-
-## Missing Import
-
-```lean broken
-def inventory :=
-  Std.HashSet.ofList [("apples", 3), ("bananas", 4)]
-```
-```output
-Unknown identifier `Std.HashSet.ofList`
-```
-```lean fixed
-public import Std.Data.HashSet.Basic
-
-public section
-
-def inventory :=
-  Std.HashSet.ofList [("apples", 3), ("bananas", 4)]
-```
-The constant `Std.HashSet.ofList` is defined in the `Std.Data.HashSet.Basic` module, which has not
-been imported in the original example. This import is suggested by the unknown identifier code
-action; once it is added, this example compiles.
-
-## Variable Not in Scope
-
-```lean broken
-example (s : IO.FS.Stream) := do
-  IO.withStdout s do
-    let text := "Hello"
-    IO.println text
-  IO.println s!"Wrote '{text}' to stream"
-```
-```output
-Unknown identifier `text`
-```
-```lean fixed
-example (s : IO.FS.Stream) := do
-  let text := "Hello"
-  IO.withStdout s do
-    IO.println text
-  IO.println s!"Wrote '{text}' to stream"
-```
-An unknown identifier error occurs on the last line of this example because the variable `text` is
-not in scope. The `let`-binding on the third line is scoped to the inner `do` block and cannot be
-accessed in the outer `do` block. Moving this binding to the outer `do` block—from which it remains
-in scope in the inner block as well—resolves the issue.
-
-## Missing Namespace
-
-```lean broken
-inductive Color where
-  | rgb (r g b : Nat)
-  | grayscale (k : Nat)
-
-def red : Color :=
-  rgb 255 0 0
-```
-```output
-Unknown identifier `rgb`
-```
-```lean fixed (title := "Fixed (qualified name)")
-inductive Color where
-  | rgb (r g b : Nat)
-  | grayscale (k : Nat)
-
-def red : Color :=
-  Color.rgb 255 0 0
-```
-```lean fixed (title := "Fixed (open namespace)")
-inductive Color where
-  | rgb (r g b : Nat)
-  | grayscale (k : Nat)
-
-open Color in
-def red : Color :=
-  rgb 255 0 0
-```
-
-In this example, the identifier `rgb` on the last line does not resolve to the `Color` constructor
-of that name. This is because the constructor's name is actually `Color.rgb`: all constructors of an
-inductive type have names in that type's namespace. Because the `Color` namespace is not open, the
-identifier `rgb` cannot be used without its namespace prefix.
-
-One way to resolve this error is to provide the fully qualified constructor name `Color.rgb`; the
-dotted-identifier notation `.rgb` can also be used, since the expected type of `.rgb 255 0 0` is
-`Color`. Alternatively, one can open the `Color` namespace and continue to omit the `Color` prefix
-from the identifier.
-
-## Protected Constant Name Without Namespace Prefix
-
-```lean broken
-protected def A.x := ()
-
-open A
-
-example := x
-```
-```output
-Unknown identifier `x`
-```
-```lean fixed (title := "Fixed (qualified name)")
-protected def A.x := ()
-
-open A
-
-example := A.x
-```
-```lean fixed (title := "Fixed (restricted open)")
-protected def A.x := ()
-
-open A (x)
-
-example := x
-```
-
-In this example, because the constant `A.x` is `protected`, it cannot be referred to by the suffix
-`x` even with the namespace `A` open. Therefore, the identifier `x` fails to resolve. Instead, to
-refer to a `protected` constant, it is necessary to include at least its innermost namespace—in this
-case, `A`. Alternatively, the *restricted opening* syntax—demonstrated in the second corrected
-example—allows a `protected` constant to be referred to by its unqualified name, without opening the
-remainder of the namespace in which it occurs (see the manual section on
-[Namespaces and Sections](lean-manual://section/namespaces-sections) for details).
-
-## Unresolvable Name Inferred by Dotted-Identifier Notation
-
-```lean broken
-def disjoinToNat (b₁ b₂ : Bool) : Nat :=
-  .toNat (b₁ || b₂)
-```
-```output
-Unknown constant `Nat.toNat`
-
-Note: Inferred this name from the expected resulting type of `.toNat`:
-  Nat
-```
-```lean fixed (title := "Fixed (generalized field notation)")
-def disjoinToNat (b₁ b₂ : Bool) : Nat :=
-  (b₁ || b₂).toNat
-```
-```lean fixed (title := "Fixed (qualified name)")
-def disjoinToNat (b₁ b₂ : Bool) : Nat :=
-  Bool.toNat (b₁ || b₂)
-```
-
-In this example, the dotted-identifier notation `.toNat` causes Lean to infer an unresolvable
-name (`Nat.toNat`). The namespace used by dotted-identifier notation is always inferred from
-the expected type of the expression in which it occurs, which—due to the type annotation on
-`disjoinToNat`—is `Nat` in this example. To use the namespace of an argument's type—as the author of
-this code seemingly intended—use *generalized field notation* as shown in the first corrected
-example. Alternatively, the correct namespace can be explicitly specified by writing the fully
-qualified function name.
-
-## Auto-bound variables
-
-```lean broken
-set_option relaxedAutoImplicit false in
-def thisBreaks (x : α₁) (y : size₁) := ()
-
-set_option autoImplicit false in
-def thisAlsoBreaks (x : α₂) (y : size₂) := ()
-```
-```output
-Unknown identifier `size₁`
-
-Note: It is not possible to treat `size₁` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`.
-Unknown identifier `α₂`
-
-Note: It is not possible to treat `α₂` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
-Unknown identifier `size₂`
-
-Note: It is not possible to treat `size₂` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
-```
-```lean fixed (title := "Fixed (modifying options)")
-set_option relaxedAutoImplicit true in
-def thisWorks (x : α₁) (y : size₁) := ()
-
-set_option autoImplicit true in
-def thisAlsoWorks (x : α₂) (y : size₂) := ()
-```
-```lean fixed (title := "Fixed (add implicit bindings for the unknown identifiers)")
-set_option relaxedAutoImplicit false in
-def thisWorks {size₁} (x : α₁) (y : size₁) := ()
-
-set_option autoImplicit false in
-def thisAlsoWorks {α₂ size₂} (x : α₂) (y : size₂) := ()
-```
-
-Lean's default behavior, when it encounters an identifier it can't identify in the type of a
-definition, is to add [automatic implicit parameters](lean-manual://section/automatic-implicit-parameters)
-for those unknown identifiers. However, many files or projects disable this feature by setting the
-`autoImplicit` or `relaxedAutoImplicit` options to `false`.
-
-Without re-enabling the `autoImplicit` or `relaxedAutoImplicit` options, the easiest way to fix
-this error is to add the unknown identifiers as [ordinary implicit parameters](lean-manual://section/implicit-functions)
-as shown in the example above.
-
--/
-register_error_explanation lean.unknownIdentifier {
-  summary := "Failed to resolve identifier to variable or constant."
-  sinceVersion := "4.23.0"
-}

src/Lean/Exception.lean

@@ -9,7 +9,7 @@ prelude
 public import Lean.InternalExceptionId
 -- This import is necessary to ensure that any users of the `throwNamedError` macros have access to
 -- all declared explanations:
-public import Lean.ErrorExplanations
+public import Lean.ErrorExplanation
 
 public section
 

src/Lean/Log.lean

@@ -8,7 +8,7 @@ module
 prelude
 -- This import is necessary to ensure that any users of the `logNamedError` macros have access to
 -- all declared explanations:
-public import Lean.ErrorExplanations
+public import Lean.ErrorExplanation
 
 public section
 

src/Lean/Meta/ACLt.lean

@@ -4,12 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.DiscrTree
-
+public import Lean.Meta.DiscrTree.Main
+import Lean.Meta.WHNF
 public section
-
 namespace Lean
 
 def Expr.ctorWeight : Expr → UInt8

src/Lean/Meta/AppBuilder.lean

@@ -4,15 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.SynthInstance
 public import Lean.Meta.DecLevel
 import Lean.Meta.SameCtorUtils
 import Lean.Data.Array
-
+import Lean.Meta.CtorRecognizer
+import Lean.Structure
 public section
-
 namespace Lean.Meta
 
 /-- Returns `id e` -/

src/Lean/Meta/Basic.lean

@@ -34,6 +34,7 @@ def TransparencyMode.toUInt64 : TransparencyMode → UInt64
   | .default   => 1
   | .reducible => 2
   | .instances => 3
+  | .none      => 4
 
 def EtaStructMode.toUInt64 : EtaStructMode → UInt64
   | .all        => 0
@@ -506,6 +507,11 @@ structure Context where
    This is not a great solution, but a proper solution would require a more sophisticated caching mechanism.
   -/
   inTypeClassResolution : Bool := false
+  /--
+  When `cacheInferType := true`, the `inferType` results are cached if the input term does not contain
+  metavariables
+  -/
+  cacheInferType : Bool := true
 deriving Inhabited
 
 def Context.config (c : Context) : Config := c.keyedConfig.config

src/Lean/Meta/Coe.lean

@@ -4,15 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.AppBuilder
 import Lean.ExtraModUses
-
+import Lean.ProjFns
+import Lean.Meta.Transform
+import Lean.Meta.WHNF
 public section
-
 namespace Lean.Meta
-
 /--
 Tags declarations to be unfolded during coercion elaboration.
 

src/Lean/Meta/CongrTheorems.lean

@@ -4,14 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.AddDecl
 public import Lean.ReservedNameAction
+import Lean.Structure
 import Lean.Meta.Tactic.Subst
-
+import Lean.Meta.FunInfo
 public section
-
 namespace Lean.Meta
 
 inductive CongrArgKind where

src/Lean/Meta/Constructions/SparseCasesOn.lean

@@ -3,16 +3,14 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joachim Breitner
 -/
-
 module
-
 prelude
 public import Lean.Meta.Basic
 import Lean.AddDecl
 import Lean.Meta.Constructions.CtorIdx
 import Lean.Meta.AppBuilder
 import Lean.Meta.HasNotBit
-
+import Lean.Meta.WHNF
 /-!  See `mkSparseCasesOn` below.  -/
 
 namespace Lean.Meta

src/Lean/Meta/DiscrTree.lean

@@ -4,874 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jannis Limperg, Kim Morrison
 -/
 module
-
 prelude
 public import Lean.Meta.WHNF
-public import Lean.Meta.DiscrTreeTypes
-
-public section
-
-namespace Lean.Meta.DiscrTree
-/-!
-  (Imperfect) discrimination trees.
-  We use a hybrid representation.
-  - A `PersistentHashMap` for the root node which usually contains many children.
-  - A sorted array of key/node pairs for inner nodes.
-
-  The edges are labeled by keys:
-  - Constant names (and arity). Universe levels are ignored.
-  - Free variables (and arity). Thus, an entry in the discrimination tree
-    may reference hypotheses from the local context.
-  - Literals
-  - Star/Wildcard. We use them to represent metavariables and terms
-    we want to ignore. We ignore implicit arguments and proofs.
-  - Other. We use to represent other kinds of terms (e.g., nested lambda, forall, sort, etc).
-
-  We reduce terms using `TransparencyMode.reducible`. Thus, all reducible
-  definitions in an expression `e` are unfolded before we insert it into the
-  discrimination tree.
-
-  Recall that projections from classes are **NOT** reducible.
-  For example, the expressions `Add.add α (ringAdd ?α ?s) ?x ?x`
-  and `Add.add Nat Nat.hasAdd a b` generates paths with the following keys
-  respectively
-  ```
-  ⟨Add.add, 4⟩, α, *, *, *
-  ⟨Add.add, 4⟩, Nat, *, ⟨a,0⟩, ⟨b,0⟩
-  ```
-
-  That is, we don't reduce `Add.add Nat inst a b` into `Nat.add a b`.
-  We say the `Add.add` applications are the de-facto canonical forms in
-  the metaprogramming framework.
-  Moreover, it is the metaprogrammer's responsibility to re-pack applications such as
-  `Nat.add a b` into `Add.add Nat inst a b`.
-
-  Remark: we store the arity in the keys
-  1- To be able to implement the "skip" operation when retrieving "candidate"
-     unifiers.
-  2- Distinguish partial applications `f a`, `f a b`, and `f a b c`.
--/
-
-def Key.lt : Key → Key → Bool
-  | .lit v₁,        .lit v₂        => v₁ < v₂
-  | .fvar n₁ a₁,    .fvar n₂ a₂    => Name.quickLt n₁.name n₂.name || (n₁ == n₂ && a₁ < a₂)
-  | .const n₁ a₁,   .const n₂ a₂   => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂)
-  | .proj s₁ i₁ a₁, .proj s₂ i₂ a₂ => Name.quickLt s₁ s₂ || (s₁ == s₂ && i₁ < i₂) || (s₁ == s₂ && i₁ == i₂ && a₁ < a₂)
-  | k₁,             k₂             => k₁.ctorIdx < k₂.ctorIdx
-
-instance : LT Key := ⟨fun a b => Key.lt a b⟩
-instance (a b : Key) : Decidable (a < b) := inferInstanceAs (Decidable (Key.lt a b))
-
-def Key.format : Key → Format
-  | .star            => "*"
-  | .other           => "◾"
-  | .lit (.natVal v) => Std.format v
-  | .lit (.strVal v) => repr v
-  | .const k _       => Std.format k
-  | .proj s i _      => Std.format s ++ "." ++ Std.format i
-  | .fvar k _        => Std.format k.name
-  | .arrow           => "∀"
-
-instance : ToFormat Key := ⟨Key.format⟩
-
-/--
-Helper function for converting an entry (i.e., `Array Key`) to the discrimination tree into
-`MessageData` that is more user-friendly. We use this function to implement diagnostic information.
--/
-partial def keysAsPattern (keys : Array Key) : CoreM MessageData := do
-  go (parenIfNonAtomic := false) |>.run' keys.toList
-where
-  next? : StateRefT (List Key) CoreM (Option Key) := do
-    let key :: keys ← get | return none
-    set keys
-    return some key
-
-  mkApp (f : MessageData) (args : Array MessageData) (parenIfNonAtomic : Bool) : CoreM MessageData := do
-    if args.isEmpty then
-      return f
-    else
-      let mut r := m!""
-      for arg in args do
-        r := r ++ Format.line ++ arg
-      r := f ++ .nest 2 r
-      if parenIfNonAtomic then
-        return .paren r
-      else
-        return .group r
-
-  go (parenIfNonAtomic := true) : StateRefT (List Key) CoreM MessageData := do
-    let some key ← next? | return .nil
-    match key with
-    | .const declName nargs =>
-      mkApp m!"{← mkConstWithLevelParams declName}" (← goN nargs) parenIfNonAtomic
-    | .fvar fvarId nargs =>
-      mkApp m!"{mkFVar fvarId}" (← goN nargs) parenIfNonAtomic
-    | .proj _ i nargs =>
-      mkApp m!"{← go}.{i+1}" (← goN nargs) parenIfNonAtomic
-    | .arrow =>
-      mkApp m!"∀ " (← goN 1) parenIfNonAtomic
-    | .star => return "_"
-    | .other => return "<other>"
-    | .lit (.natVal v) => return m!"{v}"
-    | .lit (.strVal v) => return m!"{v}"
-
-  goN (num : Nat) : StateRefT (List Key) CoreM (Array MessageData) := do
-    let mut r := #[]
-    for _ in *...num do
-      r := r.push (← go)
-    return r
-
-def Key.arity : Key → Nat
-  | .const _ a  => a
-  | .fvar _ a   => a
-  /-
-  Remark: `.arrow` used to have arity 2, and was used to encode only **non**-dependent
-  arrows. However, this feature was a recurrent source of bugs. For example, a
-  theorem about a dependent arrow can be applied to a non-dependent one. The
-  reverse direction may also happen. See issue #2835. Therefore, `.arrow` was made
-  to have arity 0. But this throws away easy to use information, and makes it so
-  that ∀ and ∃ behave quite differently. So now `.arrow` at least indexes the
-  domain of the forall (whether dependent or non-dependent).
-  -/
-  | .arrow      => 1
-  | .proj _ _ a => 1 + a
-  | _           => 0
-
-instance : Inhabited (Trie α) := ⟨.node #[] #[]⟩
-
-def empty : DiscrTree α := { root := {} }
-
-partial def Trie.format [ToFormat α] : Trie α → Format
-  | .node vs cs => Format.group $ Format.paren $
-    "node" ++ (if vs.isEmpty then Format.nil else " " ++ Std.format vs)
-    ++ Format.join (cs.toList.map fun ⟨k, c⟩ => Format.line ++ Format.paren (Std.format k ++ " => " ++ format c))
-
-instance [ToFormat α] : ToFormat (Trie α) := ⟨Trie.format⟩
-
-partial def format [ToFormat α] (d : DiscrTree α) : Format :=
-  let (_, r) := d.root.foldl
-    (fun (p : Bool × Format) k c =>
-      (false, p.2 ++ (if p.1 then Format.nil else Format.line) ++ Format.paren (Std.format k ++ " => " ++ Std.format c)))
-    (true, Format.nil)
-  Format.group r
-
-instance [ToFormat α] : ToFormat (DiscrTree α) := ⟨format⟩
-
-/-- The discrimination tree ignores implicit arguments and proofs.
-   We use the following auxiliary id as a "mark". -/
-private def tmpMVarId : MVarId := { name := `_discr_tree_tmp }
-private def tmpStar := mkMVar tmpMVarId
-
-instance : Inhabited (DiscrTree α) where
-  default := {}
-
-/--
-  Return true iff the argument should be treated as a "wildcard" by the discrimination tree.
-
-  - We ignore proofs because of proof irrelevance. It doesn't make sense to try to
-    index their structure.
-
-  - We ignore instance implicit arguments (e.g., `[Add α]`) because they are "morally" canonical.
-    Moreover, we may have many definitionally equal terms floating around.
-    Example: `Ring.hasAdd Int Int.isRing` and `Int.hasAdd`.
-
-  - We considered ignoring implicit arguments (e.g., `{α : Type}`) since users don't "see" them,
-    and may not even understand why some simplification rule is not firing.
-    However, in type class resolution, we have instance such as `Decidable (@Eq Nat x y)`,
-    where `Nat` is an implicit argument. Thus, we would add the path
-    ```
-    Decidable -> Eq -> * -> * -> * -> [Nat.decEq]
-    ```
-    to the discrimination tree IF we ignored the implicit `Nat` argument.
-    This would be BAD since **ALL** decidable equality instances would be in the same path.
-    So, we index implicit arguments if they are types.
-    This setting seems sensible for simplification theorems such as:
-    ```
-    forall (x y : Unit), (@Eq Unit x y) = true
-    ```
-    If we ignore the implicit argument `Unit`, the `DiscrTree` will say it is a candidate
-    simplification theorem for any equality in our goal.
-
-  Remark: if users have problems with the solution above, we may provide a `noIndexing` annotation,
-  and `ignoreArg` would return true for any term of the form `noIndexing t`.
--/
-private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Bool := do
-  if h : i < infos.size then
-    let info := infos[i]
-    if info.isInstImplicit then
-      return true
-    else if info.isImplicit || info.isStrictImplicit then
-      return !(← isType a)
-    else
-      isProof a
-  else
-    isProof a
-
-private partial def pushArgsAux (infos : Array ParamInfo) : Nat → Expr → Array Expr → MetaM (Array Expr)
-  | i, .app f a, todo => do
-    if (← ignoreArg a i infos) then
-      pushArgsAux infos (i-1) f (todo.push tmpStar)
-    else
-      pushArgsAux infos (i-1) f (todo.push a)
-  | _, _, todo => return todo
-
-/--
-  Return true if `e` is one of the following
-  - A nat literal (numeral)
-  - `Nat.zero`
-  - `Nat.succ x` where `isNumeral x`
-  - `OfNat.ofNat _ x _` where `isNumeral x` -/
-private partial def isNumeral (e : Expr) : Bool :=
-  if e.isRawNatLit then true
-  else
-    let f := e.getAppFn
-    if !f.isConst then false
-    else
-      let fName := f.constName!
-      if fName == ``Nat.succ && e.getAppNumArgs == 1 then isNumeral e.appArg!
-      else if fName == ``OfNat.ofNat && e.getAppNumArgs == 3 then isNumeral (e.getArg! 1)
-      else if fName == ``Nat.zero && e.getAppNumArgs == 0 then true
-      else false
-
-private partial def toNatLit? (e : Expr) : Option Literal :=
-  if isNumeral e then
-    if let some n := loop e then
-      some (.natVal n)
-    else
-      none
-  else
-    none
-where
-  loop (e : Expr) : OptionT Id Nat := do
-    let f := e.getAppFn
-    match f with
-    | .lit (.natVal n) => return n
-    | .const fName .. =>
-      if fName == ``Nat.succ && e.getAppNumArgs == 1 then
-        let r ← loop e.appArg!
-        return r+1
-      else if fName == ``OfNat.ofNat && e.getAppNumArgs == 3 then
-        loop (e.getArg! 1)
-      else if fName == ``Nat.zero && e.getAppNumArgs == 0 then
-        return 0
-      else
-        failure
-    | _ => failure
-
-private def isNatType (e : Expr) : MetaM Bool :=
-  return (← whnf e).isConstOf ``Nat
-
-/--
-  Return true if `e` is one of the following
-  - `Nat.add _ k` where `isNumeral k`
-  - `Add.add Nat _ _ k` where `isNumeral k`
-  - `HAdd.hAdd _ Nat _ _ k` where `isNumeral k`
-  - `Nat.succ _`
-  This function assumes `e.isAppOf fName`
--/
-private def isOffset (fName : Name) (e : Expr) : MetaM Bool := do
-  if fName == ``Nat.add && e.getAppNumArgs == 2 then
-    return isNumeral e.appArg!
-  else if fName == ``Add.add && e.getAppNumArgs == 4 then
-    if (← isNatType (e.getArg! 0)) then return isNumeral e.appArg! else return false
-  else if fName == ``HAdd.hAdd && e.getAppNumArgs == 6 then
-    if (← isNatType (e.getArg! 1)) then return isNumeral e.appArg! else return false
-  else
-    return fName == ``Nat.succ && e.getAppNumArgs == 1
-
-/--
-  TODO: add hook for users adding their own functions for controlling `shouldAddAsStar`
-  Different `DiscrTree` users may populate this set using, for example, attributes.
-
-  Remark: we currently tag "offset" terms as star to avoid having to add special
-  support for offset terms.
-  Example, suppose the discrimination tree contains the entry
-  `Nat.succ ?m |-> v`, and we are trying to retrieve the matches for `Expr.lit (Literal.natVal 1) _`.
-  In this scenario, we want to retrieve `Nat.succ ?m |-> v`
--/
-private def shouldAddAsStar (fName : Name) (e : Expr) : MetaM Bool := do
-  isOffset fName e
-
-def mkNoindexAnnotation (e : Expr) : Expr :=
-  mkAnnotation `noindex e
-
-def hasNoindexAnnotation (e : Expr) : Bool :=
-  annotation? `noindex e |>.isSome
-
-/--
-Reduction procedure for the discrimination tree indexing.
--/
-partial def reduce (e : Expr) : MetaM Expr := do
-  let e ← whnfCore e
-  match (← unfoldDefinition? e) with
-  | some e => reduce e
-  | none => match e.etaExpandedStrict? with
-    | some e => reduce e
-    | none   => return e
-
-/--
-  Return `true` if `fn` is a "bad" key. That is, `pushArgs` would add `Key.other` or `Key.star`.
-  We use this function when processing "root terms, and will avoid unfolding terms.
-  Note that without this trick the pattern `List.map f ∘ List.map g` would be mapped into the key `Key.other`
-  since the function composition `∘` would be unfolded and we would get `fun x => List.map g (List.map f x)`
--/
-private def isBadKey (fn : Expr) : Bool :=
-  match fn with
-  | .lit ..     => false
-  | .const ..   => false
-  | .fvar ..    => false
-  | .proj ..    => false
-  | .forallE .. => false
-  | _           => 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) : MetaM Expr := do
-  let e ← step e
-  match e.etaExpandedStrict? with
-  | some e => reduceUntilBadKey e
-  | none   => return e
-where
-  step (e : Expr) := do
-    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) : MetaM Expr :=
-  if root then reduceUntilBadKey e else reduce e
-
-/- Remark: we use `shouldAddAsStar` only for nested terms, and `root == false` for nested terms -/
-
-/--
-Append `n` wildcards to `todo`
--/
-private def pushWildcards (n : Nat) (todo : Array Expr) : Array Expr :=
-  match n with
-  | 0   => todo
-  | n+1 => pushWildcards n (todo.push tmpStar)
-
-/--
-When `noIndexAtArgs := true`, `pushArgs` assumes function application arguments have a `no_index` annotation.
-That is, `f a b` is indexed as it was `f (no_index a) (no_index b)`.
-This feature is used when indexing local proofs in the simplifier. This is useful in examples like the one described on issue #2670.
-In this issue, we have a local hypotheses `(h : ∀ p : α × β, f p p.2 = p.2)`, and users expect it to be applicable to
-`f (a, b) b = b`. This worked in Lean 3 since no indexing was used. We can retrieve Lean 3 behavior by writing
-`(h : ∀ p : α × β, f p (no_index p.2) = p.2)`, but this is very inconvenient when the hypotheses was not written by the user in first place.
-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) (noIndexAtArgs : Bool) : MetaM (Key × Array Expr) := do
-  if hasNoindexAnnotation e then
-    return (.star, todo)
-  else
-    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
-      let todo ← if noIndexAtArgs then
-        pure <| pushWildcards nargs todo
-      else
-        pushArgsAux info.paramInfo (nargs-1) e todo
-      return (k, todo)
-    match fn with
-    | .lit v     =>
-      return (.lit v, todo)
-    | .const c _ =>
-      unless root do
-        if let some v := toNatLit? e then
-          return (.lit v, todo)
-        if (← shouldAddAsStar c e) then
-          return (.star, todo)
-      let nargs := e.getAppNumArgs
-      push (.const c nargs) nargs todo
-    | .proj s i a =>
-      /-
-      If `s` is a class, then `a` is an instance. Thus, we annotate `a` with `no_index` since we do not
-      index instances. This should only happen if users mark a class projection function as `[reducible]`.
-
-      TODO: add better support for projections that are functions
-      -/
-      let a := if isClass (← getEnv) s then mkNoindexAnnotation a else a
-      let nargs := e.getAppNumArgs
-      push (.proj s i nargs) nargs (todo.push a)
-    | .fvar fvarId   =>
-      let nargs := e.getAppNumArgs
-      push (.fvar fvarId nargs) nargs todo
-    | .mvar mvarId   =>
-      if mvarId == tmpMVarId then
-        -- We use `tmp to mark implicit arguments and proofs
-        return (.star, todo)
-      else if (← mvarId.isReadOnlyOrSyntheticOpaque) then
-        return (.other, todo)
-      else
-        return (.star, todo)
-    | .forallE _n d _ _ =>
-      return (.arrow, todo.push d)
-    | _ => return (.other, todo)
-
-@[inherit_doc pushArgs]
-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 noIndexAtArgs
-    mkPathAux false todo (keys.push k) noIndexAtArgs
-
-private def initCapacity := 8
-
-@[inherit_doc pushArgs]
-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 noIndexAtArgs
-
-private partial def createNodes (keys : Array Key) (v : α) (i : Nat) : Trie α :=
-  if h : i < keys.size then
-    let k := keys[i]
-    let c := createNodes keys v (i+1)
-    .node #[] #[(k, c)]
-  else
-    .node #[v] #[]
-
-/--
-If `vs` contains an element `v'` such that `v == v'`, then replace `v'` with `v`.
-Otherwise, push `v`.
-See issue #2155
-Recall that `BEq α` may not be Lawful.
--/
-private def insertVal [BEq α] (vs : Array α) (v : α) : Array α :=
-  loop 0
-where
-  loop (i : Nat) : Array α :=
-    if h : i < vs.size then
-      if v == vs[i] then
-        vs.set i v
-      else
-        loop (i+1)
-    else
-      vs.push v
-  termination_by vs.size - i
-
-private partial def insertAux [BEq α] (keys : Array Key) (v : α) : Nat → Trie α → Trie α
-  | i, .node vs cs =>
-    if h : i < keys.size then
-      let k := keys[i]
-      let c := Id.run $ cs.binInsertM
-          (fun a b => a.1 < b.1)
-          (fun ⟨_, s⟩ => let c := insertAux keys v (i+1) s; (k, c)) -- merge with existing
-          (fun _ => let c := createNodes keys v (i+1); (k, c))
-          (k, default)
-      .node vs c
-    else
-      .node (insertVal vs v) cs
-
-def insertCore [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α :=
-  if keys.isEmpty then panic! "invalid key sequence"
-  else
-    let k := keys[0]!
-    match d.root.find? k with
-    | none =>
-      let c := createNodes keys v 1
-      { root := d.root.insert k c }
-    | some c =>
-      let c := insertAux keys v 1 c
-      { root := d.root.insert k c }
-
-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 : α) (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) : MetaM (Key × Array Expr) := do
-  let e ← reduceDT e root
-  unless root do
-    -- See pushArgs
-    if let some v := toNatLit? e then
-      return (.lit v, #[])
-  match e.getAppFn with
-  | .lit v         => return (.lit v, #[])
-  | .const c _     =>
-    if (← getConfig).isDefEqStuckEx && e.hasExprMVar then
-      if (← isReducible c) then
-        /- `e` is a term `c ...` s.t. `c` is reducible and `e` has metavariables, but it was not unfolded.
-           This can happen if the metavariables in `e` are "blocking" smart unfolding.
-           If `isDefEqStuckEx` is enabled, then we must throw the `isDefEqStuck` exception to postpone TC resolution.
-           Here is an example. Suppose we have
-           ```
-            inductive Ty where
-              | bool | fn (a ty : Ty)
-
-
-            @[reducible] def Ty.interp : Ty → Type
-              | bool   => Bool
-              | fn a b => a.interp → b.interp
-           ```
-           and we are trying to synthesize `BEq (Ty.interp ?m)`
-        -/
-        Meta.throwIsDefEqStuck
-      else if let some matcherInfo := isMatcherAppCore? (← getEnv) e then
-        -- A matcher application is stuck is one of the discriminants has a metavariable
-        let args := e.getAppArgs
-        for arg in args[matcherInfo.getFirstDiscrPos...(matcherInfo.getFirstDiscrPos + matcherInfo.numDiscrs)] do
-          if arg.hasExprMVar then
-            Meta.throwIsDefEqStuck
-      else if (← isRec c) then
-        /- Similar to the previous case, but for `match` and recursor applications. It may be stuck (i.e., did not reduce)
-           because of metavariables. -/
-        Meta.throwIsDefEqStuck
-    let nargs := e.getAppNumArgs
-    return (.const c nargs, e.getAppRevArgs)
-  | .fvar fvarId   =>
-    let nargs := e.getAppNumArgs
-    return (.fvar fvarId nargs, e.getAppRevArgs)
-  | .mvar mvarId   =>
-    if isMatch then
-      return (.other, #[])
-    else do
-      let cfg ← getConfig
-      if cfg.isDefEqStuckEx then
-        /-
-          When the configuration flag `isDefEqStuckEx` is set to true,
-          we want `isDefEq` to throw an exception whenever it tries to assign
-          a read-only metavariable.
-          This feature is useful for type class resolution where
-          we may want to notify the caller that the TC problem may be solvable
-          later after it assigns `?m`.
-          The method `DiscrTree.getUnify e` returns candidates `c` that may "unify" with `e`.
-          That is, `isDefEq c e` may return true. Now, consider `DiscrTree.getUnify d (Add ?m)`
-          where `?m` is a read-only metavariable, and the discrimination tree contains the keys
-          `HadAdd Nat` and `Add Int`. If `isDefEqStuckEx` is set to true, we must treat `?m` as
-          a regular metavariable here, otherwise we return the empty set of candidates.
-          This is incorrect because it is equivalent to saying that there is no solution even if
-          the caller assigns `?m` and try again. -/
-        return (.star, #[])
-      else if (← mvarId.isReadOnlyOrSyntheticOpaque) then
-        return (.other, #[])
-      else
-        return (.star, #[])
-  | .proj s i a .. =>
-    let nargs := e.getAppNumArgs
-    return (.proj s i nargs, #[a] ++ e.getAppRevArgs)
-  | .forallE _ d _ _ => return (.arrow, #[d])
-  | _ => return (.other, #[])
-
-private abbrev getMatchKeyArgs (e : Expr) (root : Bool) : MetaM (Key × Array Expr) :=
-  getKeyArgs e (isMatch := true) (root := root)
-
-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
-  match d.root.find? .star with
-  | none                  => result
-  | some (.node vs _) => result ++ vs
-
-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 α) : MetaM (Array α) := do
-  match c with
-  | .node vs cs =>
-    if todo.isEmpty then
-      return result ++ vs
-    else if cs.isEmpty then
-      return result
-    else
-      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)
-      /- 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
-        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
-      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 α) : MetaM (Array α) :=
-  match d.root.find? k with
-  | none   => return result
-  | some c => getMatchLoop args c result
-
-private def getMatchCore (d : DiscrTree α) (e : Expr) : MetaM (Key × Array α) :=
-  withReducible do
-    let result := getStarResult d
-    let (k, args) ← getMatchKeyArgs e (root := true)
-    match k with
-    | .star  => return (k, result)
-    | _      => return (k, (← getMatchRoot d k args result))
-
-/--
-  Find values that match `e` in `d`.
--/
-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) : MetaM (Array (α × Nat)) := do
-  let (k, result) ← getMatchCore d e
-  let result := result.map (·, 0)
-  if !e.isApp then
-    return result
-  else if !(← mayMatchPrefix k) then
-    return result
-  else
-    go e.appFn! 1 result
-where
-  mayMatchPrefix (k : Key) : MetaM Bool :=
-    let cont (k : Key) : MetaM Bool :=
-      if d.root.find? k |>.isSome then
-        return true
-      else
-        mayMatchPrefix k
-    match k with
-    | .const f (n+1)  => cont (.const f n)
-    | .fvar f (n+1)   => cont (.fvar f n)
-    | .proj s i (n+1) => cont (.proj s i n)
-    | _               => return false
-
-  go (e : Expr) (numExtra : Nat) (result : Array (α × Nat)) : MetaM (Array (α × Nat)) := do
-    let result := result ++ (← getMatchCore d e).2.map (., numExtra)
-    if e.isApp then
-      go e.appFn! (numExtra + 1) result
-    else
-      return result
-
-/--
-Return the root symbol for `e`, and the number of arguments after `reduceDT`.
--/
-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
-    | .fvar fvarId   => .fvar fvarId numArgs
-    | .mvar _        => .other
-    | .proj s i _ .. => .proj s i numArgs
-    | .forallE ..    => .arrow
-    | .const c _     =>
-      -- This method is used by the simplifier only, we do **not** support
-      -- (← getConfig).isDefEqStuckEx
-      .const c numArgs
-    | _ => .other
-  return (key, numArgs)
-
-/--
-Get all results under key `k`.
--/
-private partial def getAllValuesForKey (d : DiscrTree α) (k : Key) (result : Array α) : Array α :=
-  match d.root.find? k with
-  | none      => result
-  | some trie => go trie result
-where
-  go (trie : Trie α) (result : Array α) : Array α := Id.run do
-    match trie with
-    | .node vs cs =>
-      let mut result := result ++ vs
-      for (_, trie) in cs do
-        result := go trie result
-      return result
-
-/--
-A liberal version of `getMatch` which only takes the root symbol of `e` into account.
-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) : MetaM (Array α × Nat) := do
-  withReducible do
-    let result := getStarResult d
-    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) : MetaM (Array α) :=
-  withReducible do
-    let (k, args) ← getUnifyKeyArgs e (root := true)
-    match k with
-    | .star => d.root.foldlM (init := #[]) fun result k c => process k.arity #[] c result
-    | _ =>
-      let result := getStarResult d
-      match d.root.find? k with
-      | none   => return result
-      | some c => process 0 args c result
-where
-  process (skip : Nat) (todo : Array Expr) (c : Trie α) (result : Array α) : MetaM (Array α) := do
-    match skip, c with
-    | skip+1, .node _  cs =>
-      if cs.isEmpty then
-        return result
-      else
-        cs.foldlM (init := result) fun result ⟨k, c⟩ => process (skip + k.arity) todo c result
-    | 0, .node vs cs => do
-      if todo.isEmpty then
-        return result ++ vs
-      else if cs.isEmpty then
-        return result
-      else
-        let e     := todo.back!
-        let todo  := todo.pop
-        let (k, args) ← getUnifyKeyArgs e (root := false)
-        let visitStar (result : Array α) : MetaM (Array α) :=
-          let first := cs[0]!
-          if first.1 == .star then
-            process 0 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 => process 0 (todo ++ args) c.2 result
-        match k with
-        | .star  => cs.foldlM (init := result) fun result ⟨k, c⟩ => process k.arity todo c result
-        | _      => visitNonStar k args (← visitStar result)
-
-namespace Trie
-
-/--
-Monadically fold the keys and values stored in a `Trie`.
--/
-partial def foldM [Monad m] (initialKeys : Array Key)
-    (f : σ → Array Key → α → m σ) : (init : σ) → Trie α → m σ
-  | init, Trie.node vs children => do
-    let s ← vs.foldlM (init := init) fun s v => f s initialKeys v
-    children.foldlM (init := s) fun s (k, t) =>
-      t.foldM (initialKeys.push k) f s
-
-/--
-Fold the keys and values stored in a `Trie`.
--/
-@[inline]
-def fold (initialKeys : Array Key) (f : σ → Array Key → α → σ) (init : σ) (t : Trie α) : σ :=
-  Id.run <| t.foldM initialKeys (init := init) fun s k a => return f s k a
-
-/--
-Monadically fold the values stored in a `Trie`.
--/
-partial def foldValuesM [Monad m] (f : σ → α → m σ) : (init : σ) → Trie α → m σ
-  | init, node vs children => do
-    let s ← vs.foldlM (init := init) f
-    children.foldlM (init := s) fun s (_, c) => c.foldValuesM (init := s) f
-
-/--
-Fold the values stored in a `Trie`.
--/
-@[inline]
-def foldValues (f : σ → α → σ) (init : σ) (t : Trie α) : σ :=
-  Id.run <| t.foldValuesM (init := init) (pure <| f · ·)
-
-/--
-The number of values stored in a `Trie`.
--/
-partial def size : Trie α → Nat
-  | Trie.node vs children =>
-    children.foldl (init := vs.size) fun n (_, c) => n + size c
-
-end Trie
-
-
-/--
-Monadically fold over the keys and values stored in a `DiscrTree`.
--/
-@[inline]
-def foldM [Monad m] (f : σ → Array Key → α → m σ) (init : σ)
-    (t : DiscrTree α) : m σ :=
-  t.root.foldlM (init := init) fun s k t => t.foldM #[k] (init := s) f
-
-/--
-Fold over the keys and values stored in a `DiscrTree`
--/
-@[inline]
-def fold (f : σ → Array Key → α → σ) (init : σ) (t : DiscrTree α) : σ :=
-  Id.run <| t.foldM (init := init) fun s keys a => return f s keys a
-
-/--
-Monadically fold over the values stored in a `DiscrTree`.
--/
-@[inline]
-def foldValuesM [Monad m] (f : σ → α → m σ) (init : σ) (t : DiscrTree α) :
-    m σ :=
-  t.root.foldlM (init := init) fun s _ t => t.foldValuesM (init := s) f
-
-/--
-Fold over the values stored in a `DiscrTree`.
--/
-@[inline]
-def foldValues (f : σ → α → σ) (init : σ) (t : DiscrTree α) : σ :=
-  Id.run <| t.foldValuesM (init := init) (pure <| f · ·)
-
-/--
-Check for the presence of a value satisfying a predicate.
--/
-@[inline]
-def containsValueP (t : DiscrTree α) (f : α → Bool) : Bool :=
-  t.foldValues (init := false) fun r a => r || f a
-
-/--
-Extract the values stored in a `DiscrTree`.
--/
-@[inline]
-def values (t : DiscrTree α) : Array α :=
-  t.foldValues (init := #[]) fun as a => as.push a
-
-/--
-Extract the keys and values stored in a `DiscrTree`.
--/
-@[inline]
-def toArray (t : DiscrTree α) : Array (Array Key × α) :=
-  t.fold (init := #[]) fun as keys a => as.push (keys, a)
-
-/--
-Get the number of values stored in a `DiscrTree`. O(n) in the size of the tree.
--/
-@[inline]
-def size (t : DiscrTree α) : Nat :=
-  t.root.foldl (init := 0) fun n _ t => n + t.size
-
-variable {m : Type → Type} [Monad m]
-
-/-- Apply a monadic function to the array of values at each node in a `DiscrTree`. -/
-partial def Trie.mapArraysM (t : DiscrTree.Trie α) (f : Array α → m (Array β)) :
-    m (DiscrTree.Trie β) :=
-  match t with
-  | .node vs children =>
-    return .node (← f vs) (← children.mapM fun (k, t') => do pure (k, ← t'.mapArraysM f))
-
-/-- Apply a monadic function to the array of values at each node in a `DiscrTree`. -/
-def mapArraysM (d : DiscrTree α) (f : Array α → m (Array β)) : m (DiscrTree β) := do
-  pure { root := ← d.root.mapM (fun t => t.mapArraysM f) }
-
-/-- Apply a function to the array of values at each node in a `DiscrTree`. -/
-def mapArrays (d : DiscrTree α) (f : Array α → Array β) : DiscrTree β :=
-  Id.run <| d.mapArraysM fun A => pure (f A)
+public import Lean.Meta.DiscrTree.Basic
+public import Lean.Meta.DiscrTree.Util
+public import Lean.Meta.DiscrTree.Main

src/Lean/Meta/DiscrTree/Basic.lean

@@ -0,0 +1,180 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.DiscrTree.Types
+public import Lean.ToExpr
+public import Lean.CoreM
+public section
+namespace Lean.Meta.DiscrTree
+
+def mkNoindexAnnotation (e : Expr) : Expr :=
+  mkAnnotation `noindex e
+
+def hasNoindexAnnotation (e : Expr) : Bool :=
+  annotation? `noindex e |>.isSome
+
+instance : Inhabited (Trie α) where
+  default := .node #[] #[]
+
+instance : Inhabited (DiscrTree α) where
+  default := {}
+
+def empty : DiscrTree α := { root := {} }
+
+instance : ToExpr Key where
+  toTypeExpr := mkConst ``Key
+  toExpr k   := match k with
+   | .const n a => mkApp2 (mkConst ``Key.const) (toExpr n) (toExpr a)
+   | .fvar id a => mkApp2 (mkConst ``Key.fvar) (toExpr id) (toExpr a)
+   | .lit l => mkApp (mkConst ``Key.lit) (toExpr l)
+   | .star => mkConst ``Key.star
+   | .other => mkConst ``Key.other
+   | .arrow => mkConst ``Key.arrow
+   | .proj n i a => mkApp3 (mkConst ``Key.proj) (toExpr n) (toExpr i) (toExpr a)
+
+def Key.lt : Key → Key → Bool
+  | .lit v₁,        .lit v₂        => v₁ < v₂
+  | .fvar n₁ a₁,    .fvar n₂ a₂    => Name.quickLt n₁.name n₂.name || (n₁ == n₂ && a₁ < a₂)
+  | .const n₁ a₁,   .const n₂ a₂   => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂)
+  | .proj s₁ i₁ a₁, .proj s₂ i₂ a₂ => Name.quickLt s₁ s₂ || (s₁ == s₂ && i₁ < i₂) || (s₁ == s₂ && i₁ == i₂ && a₁ < a₂)
+  | k₁,             k₂             => k₁.ctorIdx < k₂.ctorIdx
+
+instance : LT Key := ⟨fun a b => Key.lt a b⟩
+instance (a b : Key) : Decidable (a < b) := inferInstanceAs (Decidable (Key.lt a b))
+
+def Key.format : Key → Format
+  | .star            => "*"
+  | .other           => "◾"
+  | .lit (.natVal v) => Std.format v
+  | .lit (.strVal v) => repr v
+  | .const k _       => Std.format k
+  | .proj s i _      => Std.format s ++ "." ++ Std.format i
+  | .fvar k _        => Std.format k.name
+  | .arrow           => "∀"
+
+instance : ToFormat Key := ⟨Key.format⟩
+
+partial def Trie.format [ToFormat α] : Trie α → Format
+  | .node vs cs => Format.group $ Format.paren $
+    "node" ++ (if vs.isEmpty then Format.nil else " " ++ Std.format vs)
+    ++ Format.join (cs.toList.map fun ⟨k, c⟩ => Format.line ++ Format.paren (Std.format k ++ " => " ++ format c))
+
+instance [ToFormat α] : ToFormat (Trie α) := ⟨Trie.format⟩
+
+partial def format [ToFormat α] (d : DiscrTree α) : Format :=
+  let (_, r) := d.root.foldl
+    (fun (p : Bool × Format) k c =>
+      (false, p.2 ++ (if p.1 then Format.nil else Format.line) ++ Format.paren (Std.format k ++ " => " ++ Std.format c)))
+    (true, Format.nil)
+  Format.group r
+
+instance [ToFormat α] : ToFormat (DiscrTree α) := ⟨format⟩
+
+/--
+Helper function for converting an entry (i.e., `Array Key`) to the discrimination tree into
+`MessageData` that is more user-friendly. We use this function to implement diagnostic information.
+-/
+partial def keysAsPattern (keys : Array Key) : CoreM MessageData := do
+  go (parenIfNonAtomic := false) |>.run' keys.toList
+where
+  next? : StateRefT (List Key) CoreM (Option Key) := do
+    let key :: keys ← get | return none
+    set keys
+    return some key
+
+  mkApp (f : MessageData) (args : Array MessageData) (parenIfNonAtomic : Bool) : CoreM MessageData := do
+    if args.isEmpty then
+      return f
+    else
+      let mut r := m!""
+      for arg in args do
+        r := r ++ Format.line ++ arg
+      r := f ++ .nest 2 r
+      if parenIfNonAtomic then
+        return .paren r
+      else
+        return .group r
+
+  go (parenIfNonAtomic := true) : StateRefT (List Key) CoreM MessageData := do
+    let some key ← next? | return .nil
+    match key with
+    | .const declName nargs =>
+      mkApp m!"{← mkConstWithLevelParams declName}" (← goN nargs) parenIfNonAtomic
+    | .fvar fvarId nargs =>
+      mkApp m!"{mkFVar fvarId}" (← goN nargs) parenIfNonAtomic
+    | .proj _ i nargs =>
+      mkApp m!"{← go}.{i+1}" (← goN nargs) parenIfNonAtomic
+    | .arrow =>
+      mkApp m!"∀ " (← goN 1) parenIfNonAtomic
+    | .star => return "_"
+    | .other => return "<other>"
+    | .lit (.natVal v) => return m!"{v}"
+    | .lit (.strVal v) => return m!"{v}"
+
+  goN (num : Nat) : StateRefT (List Key) CoreM (Array MessageData) := do
+    let mut r := #[]
+    for _ in *...num do
+      r := r.push (← go)
+    return r
+
+private partial def createNodes (keys : Array Key) (v : α) (i : Nat) : Trie α :=
+  if h : i < keys.size then
+    let k := keys[i]
+    let c := createNodes keys v (i+1)
+    .node #[] #[(k, c)]
+  else
+    .node #[v] #[]
+
+/--
+If `vs` contains an element `v'` such that `v == v'`, then replace `v'` with `v`.
+Otherwise, push `v`.
+See issue #2155
+Recall that `BEq α` may not be Lawful.
+-/
+private def insertVal [BEq α] (vs : Array α) (v : α) : Array α :=
+  loop 0
+where
+  loop (i : Nat) : Array α :=
+    if h : i < vs.size then
+      if v == vs[i] then
+        vs.set i v
+      else
+        loop (i+1)
+    else
+      vs.push v
+  termination_by vs.size - i
+
+private partial def insertAux [BEq α] (keys : Array Key) (v : α) : Nat → Trie α → Trie α
+  | i, .node vs cs =>
+    if h : i < keys.size then
+      let k := keys[i]
+      let c := Id.run $ cs.binInsertM
+          (fun a b => a.1 < b.1)
+          (fun ⟨_, s⟩ => let c := insertAux keys v (i+1) s; (k, c)) -- merge with existing
+          (fun _ => let c := createNodes keys v (i+1); (k, c))
+          (k, default)
+      .node vs c
+    else
+      .node (insertVal vs v) cs
+
+def insertKeyValue [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α :=
+  if keys.isEmpty then panic! "invalid key sequence"
+  else
+    let k := keys[0]!
+    match d.root.find? k with
+    | none =>
+      let c := createNodes keys v 1
+      { root := d.root.insert k c }
+    | some c =>
+      let c := insertAux keys v 1 c
+      { root := d.root.insert k c }
+
+@[deprecated insertKeyValue (since := "2026-01-02")]
+def insertCore [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α :=
+  insertKeyValue d keys v
+
+end Lean.Meta.DiscrTree

src/Lean/Meta/DiscrTree/Main.lean

@@ -0,0 +1,608 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Jannis Limperg, Kim Morrison
+-/
+module
+prelude
+public import Lean.Meta.Basic
+public import Lean.Meta.DiscrTree.Basic
+import Lean.Meta.WHNF
+public section
+namespace Lean.Meta.DiscrTree
+/-!
+  (Imperfect) discrimination trees.
+  We use a hybrid representation.
+  - A `PersistentHashMap` for the root node which usually contains many children.
+  - A sorted array of key/node pairs for inner nodes.
+
+  The edges are labeled by keys:
+  - Constant names (and arity). Universe levels are ignored.
+  - Free variables (and arity). Thus, an entry in the discrimination tree
+    may reference hypotheses from the local context.
+  - Literals
+  - Star/Wildcard. We use them to represent metavariables and terms
+    we want to ignore. We ignore implicit arguments and proofs.
+  - Other. We use to represent other kinds of terms (e.g., nested lambda, forall, sort, etc).
+
+  We reduce terms using `TransparencyMode.reducible`. Thus, all reducible
+  definitions in an expression `e` are unfolded before we insert it into the
+  discrimination tree.
+
+  Recall that projections from classes are **NOT** reducible.
+  For example, the expressions `Add.add α (ringAdd ?α ?s) ?x ?x`
+  and `Add.add Nat Nat.hasAdd a b` generates paths with the following keys
+  respectively
+  ```
+  ⟨Add.add, 4⟩, α, *, *, *
+  ⟨Add.add, 4⟩, Nat, *, ⟨a,0⟩, ⟨b,0⟩
+  ```
+
+  That is, we don't reduce `Add.add Nat inst a b` into `Nat.add a b`.
+  We say the `Add.add` applications are the de-facto canonical forms in
+  the metaprogramming framework.
+  Moreover, it is the metaprogrammer's responsibility to re-pack applications such as
+  `Nat.add a b` into `Add.add Nat inst a b`.
+
+  Remark: we store the arity in the keys
+  1- To be able to implement the "skip" operation when retrieving "candidate"
+     unifiers.
+  2- Distinguish partial applications `f a`, `f a b`, and `f a b c`.
+-/
+
+def Key.arity : Key → Nat
+  | .const _ a  => a
+  | .fvar _ a   => a
+  /-
+  Remark: `.arrow` used to have arity 2, and was used to encode only **non**-dependent
+  arrows. However, this feature was a recurrent source of bugs. For example, a
+  theorem about a dependent arrow can be applied to a non-dependent one. The
+  reverse direction may also happen. See issue #2835. Therefore, `.arrow` was made
+  to have arity 0. But this throws away easy to use information, and makes it so
+  that ∀ and ∃ behave quite differently. So now `.arrow` at least indexes the
+  domain of the forall (whether dependent or non-dependent).
+  -/
+  | .arrow      => 1
+  | .proj _ _ a => 1 + a
+  | _           => 0
+
+/-- The discrimination tree ignores implicit arguments and proofs.
+   We use the following auxiliary id as a "mark". -/
+private def tmpMVarId : MVarId := { name := `_discr_tree_tmp }
+private def tmpStar := mkMVar tmpMVarId
+
+/--
+  Return true iff the argument should be treated as a "wildcard" by the discrimination tree.
+
+  - We ignore proofs because of proof irrelevance. It doesn't make sense to try to
+    index their structure.
+
+  - We ignore instance implicit arguments (e.g., `[Add α]`) because they are "morally" canonical.
+    Moreover, we may have many definitionally equal terms floating around.
+    Example: `Ring.hasAdd Int Int.isRing` and `Int.hasAdd`.
+
+  - We considered ignoring implicit arguments (e.g., `{α : Type}`) since users don't "see" them,
+    and may not even understand why some simplification rule is not firing.
+    However, in type class resolution, we have instance such as `Decidable (@Eq Nat x y)`,
+    where `Nat` is an implicit argument. Thus, we would add the path
+    ```
+    Decidable -> Eq -> * -> * -> * -> [Nat.decEq]
+    ```
+    to the discrimination tree IF we ignored the implicit `Nat` argument.
+    This would be BAD since **ALL** decidable equality instances would be in the same path.
+    So, we index implicit arguments if they are types.
+    This setting seems sensible for simplification theorems such as:
+    ```
+    forall (x y : Unit), (@Eq Unit x y) = true
+    ```
+    If we ignore the implicit argument `Unit`, the `DiscrTree` will say it is a candidate
+    simplification theorem for any equality in our goal.
+
+  Remark: if users have problems with the solution above, we may provide a `noIndexing` annotation,
+  and `ignoreArg` would return true for any term of the form `noIndexing t`.
+-/
+private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Bool := do
+  if h : i < infos.size then
+    let info := infos[i]
+    if info.isInstImplicit then
+      return true
+    else if info.isImplicit || info.isStrictImplicit then
+      return !(← isType a)
+    else
+      isProof a
+  else
+    isProof a
+
+private partial def pushArgsAux (infos : Array ParamInfo) : Nat → Expr → Array Expr → MetaM (Array Expr)
+  | i, .app f a, todo => do
+    if (← ignoreArg a i infos) then
+      pushArgsAux infos (i-1) f (todo.push tmpStar)
+    else
+      pushArgsAux infos (i-1) f (todo.push a)
+  | _, _, todo => return todo
+
+/--
+  Return true if `e` is one of the following
+  - A nat literal (numeral)
+  - `Nat.zero`
+  - `Nat.succ x` where `isNumeral x`
+  - `OfNat.ofNat _ x _` where `isNumeral x` -/
+private partial def isNumeral (e : Expr) : Bool :=
+  if e.isRawNatLit then true
+  else
+    let f := e.getAppFn
+    if !f.isConst then false
+    else
+      let fName := f.constName!
+      if fName == ``Nat.succ && e.getAppNumArgs == 1 then isNumeral e.appArg!
+      else if fName == ``OfNat.ofNat && e.getAppNumArgs == 3 then isNumeral (e.getArg! 1)
+      else if fName == ``Nat.zero && e.getAppNumArgs == 0 then true
+      else false
+
+private partial def toNatLit? (e : Expr) : Option Literal :=
+  if isNumeral e then
+    if let some n := loop e then
+      some (.natVal n)
+    else
+      none
+  else
+    none
+where
+  loop (e : Expr) : OptionT Id Nat := do
+    let f := e.getAppFn
+    match f with
+    | .lit (.natVal n) => return n
+    | .const fName .. =>
+      if fName == ``Nat.succ && e.getAppNumArgs == 1 then
+        let r ← loop e.appArg!
+        return r+1
+      else if fName == ``OfNat.ofNat && e.getAppNumArgs == 3 then
+        loop (e.getArg! 1)
+      else if fName == ``Nat.zero && e.getAppNumArgs == 0 then
+        return 0
+      else
+        failure
+    | _ => failure
+
+private def isNatType (e : Expr) : MetaM Bool :=
+  return (← whnf e).isConstOf ``Nat
+
+/--
+  Return true if `e` is one of the following
+  - `Nat.add _ k` where `isNumeral k`
+  - `Add.add Nat _ _ k` where `isNumeral k`
+  - `HAdd.hAdd _ Nat _ _ k` where `isNumeral k`
+  - `Nat.succ _`
+  This function assumes `e.isAppOf fName`
+-/
+private def isOffset (fName : Name) (e : Expr) : MetaM Bool := do
+  if fName == ``Nat.add && e.getAppNumArgs == 2 then
+    return isNumeral e.appArg!
+  else if fName == ``Add.add && e.getAppNumArgs == 4 then
+    if (← isNatType (e.getArg! 0)) then return isNumeral e.appArg! else return false
+  else if fName == ``HAdd.hAdd && e.getAppNumArgs == 6 then
+    if (← isNatType (e.getArg! 1)) then return isNumeral e.appArg! else return false
+  else
+    return fName == ``Nat.succ && e.getAppNumArgs == 1
+
+/--
+  TODO: add hook for users adding their own functions for controlling `shouldAddAsStar`
+  Different `DiscrTree` users may populate this set using, for example, attributes.
+
+  Remark: we currently tag "offset" terms as star to avoid having to add special
+  support for offset terms.
+  Example, suppose the discrimination tree contains the entry
+  `Nat.succ ?m |-> v`, and we are trying to retrieve the matches for `Expr.lit (Literal.natVal 1) _`.
+  In this scenario, we want to retrieve `Nat.succ ?m |-> v`
+-/
+private def shouldAddAsStar (fName : Name) (e : Expr) : MetaM Bool := do
+  isOffset fName e
+
+/--
+Reduction procedure for the discrimination tree indexing.
+-/
+partial def reduce (e : Expr) : MetaM Expr := do
+  let e ← whnfCore e
+  match (← unfoldDefinition? e) with
+  | some e => reduce e
+  | none => match e.etaExpandedStrict? with
+    | some e => reduce e
+    | none   => return e
+
+/--
+  Return `true` if `fn` is a "bad" key. That is, `pushArgs` would add `Key.other` or `Key.star`.
+  We use this function when processing "root terms, and will avoid unfolding terms.
+  Note that without this trick the pattern `List.map f ∘ List.map g` would be mapped into the key `Key.other`
+  since the function composition `∘` would be unfolded and we would get `fun x => List.map g (List.map f x)`
+-/
+private def isBadKey (fn : Expr) : Bool :=
+  match fn with
+  | .lit ..     => false
+  | .const ..   => false
+  | .fvar ..    => false
+  | .proj ..    => false
+  | .forallE .. => false
+  | _           => 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) : MetaM Expr := do
+  let e ← step e
+  match e.etaExpandedStrict? with
+  | some e => reduceUntilBadKey e
+  | none   => return e
+where
+  step (e : Expr) := do
+    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) : MetaM Expr :=
+  if root then reduceUntilBadKey e else reduce e
+
+/- Remark: we use `shouldAddAsStar` only for nested terms, and `root == false` for nested terms -/
+
+/--
+Append `n` wildcards to `todo`
+-/
+private def pushWildcards (n : Nat) (todo : Array Expr) : Array Expr :=
+  match n with
+  | 0   => todo
+  | n+1 => pushWildcards n (todo.push tmpStar)
+
+/--
+When `noIndexAtArgs := true`, `pushArgs` assumes function application arguments have a `no_index` annotation.
+That is, `f a b` is indexed as it was `f (no_index a) (no_index b)`.
+This feature is used when indexing local proofs in the simplifier. This is useful in examples like the one described on issue #2670.
+In this issue, we have a local hypotheses `(h : ∀ p : α × β, f p p.2 = p.2)`, and users expect it to be applicable to
+`f (a, b) b = b`. This worked in Lean 3 since no indexing was used. We can retrieve Lean 3 behavior by writing
+`(h : ∀ p : α × β, f p (no_index p.2) = p.2)`, but this is very inconvenient when the hypotheses was not written by the user in first place.
+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) (noIndexAtArgs : Bool) : MetaM (Key × Array Expr) := do
+  if hasNoindexAnnotation e then
+    return (.star, todo)
+  else
+    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
+      let todo ← if noIndexAtArgs then
+        pure <| pushWildcards nargs todo
+      else
+        pushArgsAux info.paramInfo (nargs-1) e todo
+      return (k, todo)
+    match fn with
+    | .lit v     =>
+      return (.lit v, todo)
+    | .const c _ =>
+      unless root do
+        if let some v := toNatLit? e then
+          return (.lit v, todo)
+        if (← shouldAddAsStar c e) then
+          return (.star, todo)
+      let nargs := e.getAppNumArgs
+      push (.const c nargs) nargs todo
+    | .proj s i a =>
+      /-
+      If `s` is a class, then `a` is an instance. Thus, we annotate `a` with `no_index` since we do not
+      index instances. This should only happen if users mark a class projection function as `[reducible]`.
+
+      TODO: add better support for projections that are functions
+      -/
+      let a := if isClass (← getEnv) s then mkNoindexAnnotation a else a
+      let nargs := e.getAppNumArgs
+      push (.proj s i nargs) nargs (todo.push a)
+    | .fvar fvarId   =>
+      let nargs := e.getAppNumArgs
+      push (.fvar fvarId nargs) nargs todo
+    | .mvar mvarId   =>
+      if mvarId == tmpMVarId then
+        -- We use `tmp to mark implicit arguments and proofs
+        return (.star, todo)
+      else if (← mvarId.isReadOnlyOrSyntheticOpaque) then
+        return (.other, todo)
+      else
+        return (.star, todo)
+    | .forallE _n d _ _ =>
+      return (.arrow, todo.push d)
+    | _ => return (.other, todo)
+
+@[inherit_doc pushArgs]
+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 noIndexAtArgs
+    mkPathAux false todo (keys.push k) noIndexAtArgs
+
+private def initCapacity := 8
+
+@[inherit_doc pushArgs]
+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 noIndexAtArgs
+
+def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (noIndexAtArgs := false) : MetaM (DiscrTree α) := do
+  let keys ← mkPath e noIndexAtArgs
+  return d.insertKeyValue 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 : α) (noIndexAtArgs := false) : MetaM (DiscrTree α) := do
+  let keys ← mkPath e noIndexAtArgs
+  if keys == #[Key.star] || keys == #[Key.const `Eq 3, Key.star, Key.star, Key.star] then
+    return d
+  else
+    return d.insertKeyValue keys v
+
+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
+      return (.lit v, #[])
+  match e.getAppFn with
+  | .lit v         => return (.lit v, #[])
+  | .const c _     =>
+    if (← getConfig).isDefEqStuckEx && e.hasExprMVar then
+      if (← isReducible c) then
+        /- `e` is a term `c ...` s.t. `c` is reducible and `e` has metavariables, but it was not unfolded.
+           This can happen if the metavariables in `e` are "blocking" smart unfolding.
+           If `isDefEqStuckEx` is enabled, then we must throw the `isDefEqStuck` exception to postpone TC resolution.
+           Here is an example. Suppose we have
+           ```
+            inductive Ty where
+              | bool | fn (a ty : Ty)
+
+
+            @[reducible] def Ty.interp : Ty → Type
+              | bool   => Bool
+              | fn a b => a.interp → b.interp
+           ```
+           and we are trying to synthesize `BEq (Ty.interp ?m)`
+        -/
+        Meta.throwIsDefEqStuck
+      else if let some matcherInfo := isMatcherAppCore? (← getEnv) e then
+        -- A matcher application is stuck is one of the discriminants has a metavariable
+        let args := e.getAppArgs
+        for arg in args[matcherInfo.getFirstDiscrPos...(matcherInfo.getFirstDiscrPos + matcherInfo.numDiscrs)] do
+          if arg.hasExprMVar then
+            Meta.throwIsDefEqStuck
+      else if (← isRec c) then
+        /- Similar to the previous case, but for `match` and recursor applications. It may be stuck (i.e., did not reduce)
+           because of metavariables. -/
+        Meta.throwIsDefEqStuck
+    let nargs := e.getAppNumArgs
+    return (.const c nargs, e.getAppRevArgs)
+  | .fvar fvarId   =>
+    let nargs := e.getAppNumArgs
+    return (.fvar fvarId nargs, e.getAppRevArgs)
+  | .mvar mvarId   =>
+    if isMatch then
+      return (.other, #[])
+    else do
+      let cfg ← getConfig
+      if cfg.isDefEqStuckEx then
+        /-
+          When the configuration flag `isDefEqStuckEx` is set to true,
+          we want `isDefEq` to throw an exception whenever it tries to assign
+          a read-only metavariable.
+          This feature is useful for type class resolution where
+          we may want to notify the caller that the TC problem may be solvable
+          later after it assigns `?m`.
+          The method `DiscrTree.getUnify e` returns candidates `c` that may "unify" with `e`.
+          That is, `isDefEq c e` may return true. Now, consider `DiscrTree.getUnify d (Add ?m)`
+          where `?m` is a read-only metavariable, and the discrimination tree contains the keys
+          `HadAdd Nat` and `Add Int`. If `isDefEqStuckEx` is set to true, we must treat `?m` as
+          a regular metavariable here, otherwise we return the empty set of candidates.
+          This is incorrect because it is equivalent to saying that there is no solution even if
+          the caller assigns `?m` and try again. -/
+        return (.star, #[])
+      else if (← mvarId.isReadOnlyOrSyntheticOpaque) then
+        return (.other, #[])
+      else
+        return (.star, #[])
+  | .proj s i a .. =>
+    let nargs := e.getAppNumArgs
+    return (.proj s i nargs, #[a] ++ e.getAppRevArgs)
+  | .forallE _ d _ _ => return (.arrow, #[d])
+  | _ => return (.other, #[])
+
+private abbrev getMatchKeyArgs (e : Expr) (root : Bool) : MetaM (Key × Array Expr) :=
+  getKeyArgs e (isMatch := true) (root := root)
+
+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
+  match d.root.find? .star with
+  | none                  => result
+  | some (.node vs _) => result ++ vs
+
+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 α) : MetaM (Array α) := do
+  match c with
+  | .node vs cs =>
+    if todo.isEmpty then
+      return result ++ vs
+    else if cs.isEmpty then
+      return result
+    else
+      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)
+      /- 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
+        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
+      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 α) : MetaM (Array α) :=
+  match d.root.find? k with
+  | none   => return result
+  | some c => getMatchLoop args c result
+
+private def getMatchCore (d : DiscrTree α) (e : Expr) : MetaM (Key × Array α) :=
+  withReducible do
+    let result := getStarResult d
+    let (k, args) ← getMatchKeyArgs e (root := true)
+    match k with
+    | .star  => return (k, result)
+    | _      => return (k, (← getMatchRoot d k args result))
+
+/--
+  Find values that match `e` in `d`.
+-/
+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) : MetaM (Array (α × Nat)) := do
+  let (k, result) ← getMatchCore d e
+  let result := result.map (·, 0)
+  if !e.isApp then
+    return result
+  else if !(← mayMatchPrefix k) then
+    return result
+  else
+    go e.appFn! 1 result
+where
+  mayMatchPrefix (k : Key) : MetaM Bool :=
+    let cont (k : Key) : MetaM Bool :=
+      if d.root.find? k |>.isSome then
+        return true
+      else
+        mayMatchPrefix k
+    match k with
+    | .const f (n+1)  => cont (.const f n)
+    | .fvar f (n+1)   => cont (.fvar f n)
+    | .proj s i (n+1) => cont (.proj s i n)
+    | _               => return false
+
+  go (e : Expr) (numExtra : Nat) (result : Array (α × Nat)) : MetaM (Array (α × Nat)) := do
+    let result := result ++ (← getMatchCore d e).2.map (., numExtra)
+    if e.isApp then
+      go e.appFn! (numExtra + 1) result
+    else
+      return result
+
+/--
+Return the root symbol for `e`, and the number of arguments after `reduceDT`.
+-/
+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
+    | .fvar fvarId   => .fvar fvarId numArgs
+    | .mvar _        => .other
+    | .proj s i _ .. => .proj s i numArgs
+    | .forallE ..    => .arrow
+    | .const c _     =>
+      -- This method is used by the simplifier only, we do **not** support
+      -- (← getConfig).isDefEqStuckEx
+      .const c numArgs
+    | _ => .other
+  return (key, numArgs)
+
+/--
+Get all results under key `k`.
+-/
+private partial def getAllValuesForKey (d : DiscrTree α) (k : Key) (result : Array α) : Array α :=
+  match d.root.find? k with
+  | none      => result
+  | some trie => go trie result
+where
+  go (trie : Trie α) (result : Array α) : Array α := Id.run do
+    match trie with
+    | .node vs cs =>
+      let mut result := result ++ vs
+      for (_, trie) in cs do
+        result := go trie result
+      return result
+
+/--
+A liberal version of `getMatch` which only takes the root symbol of `e` into account.
+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) : MetaM (Array α × Nat) := do
+  withReducible do
+    let result := getStarResult d
+    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) : MetaM (Array α) :=
+  withReducible do
+    let (k, args) ← getUnifyKeyArgs e (root := true)
+    match k with
+    | .star => d.root.foldlM (init := #[]) fun result k c => process k.arity #[] c result
+    | _ =>
+      let result := getStarResult d
+      match d.root.find? k with
+      | none   => return result
+      | some c => process 0 args c result
+where
+  process (skip : Nat) (todo : Array Expr) (c : Trie α) (result : Array α) : MetaM (Array α) := do
+    match skip, c with
+    | skip+1, .node _  cs =>
+      if cs.isEmpty then
+        return result
+      else
+        cs.foldlM (init := result) fun result ⟨k, c⟩ => process (skip + k.arity) todo c result
+    | 0, .node vs cs => do
+      if todo.isEmpty then
+        return result ++ vs
+      else if cs.isEmpty then
+        return result
+      else
+        let e     := todo.back!
+        let todo  := todo.pop
+        let (k, args) ← getUnifyKeyArgs e (root := false)
+        let visitStar (result : Array α) : MetaM (Array α) :=
+          let first := cs[0]!
+          if first.1 == .star then
+            process 0 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 => process 0 (todo ++ args) c.2 result
+        match k with
+        | .star  => cs.foldlM (init := result) fun result ⟨k, c⟩ => process k.arity todo c result
+        | _      => visitNonStar k args (← visitStar result)
+
+end Lean.Meta.DiscrTree

src/Lean/Meta/DiscrTree/Types.lean

@@ -4,16 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.ToExpr
-
+public import Lean.Expr
 public section
-
 namespace Lean.Meta
-
 /-! See file `DiscrTree.lean` for the actual implementation and documentation. -/
-
 namespace DiscrTree
 /--
 Discrimination tree key. See `DiscrTree`
@@ -39,17 +34,6 @@ protected def Key.hash : Key → UInt64
 
 instance : Hashable Key := ⟨Key.hash⟩
 
-instance : ToExpr Key where
-  toTypeExpr := mkConst ``Key
-  toExpr k   := match k with
-   | .const n a => mkApp2 (mkConst ``Key.const) (toExpr n) (toExpr a)
-   | .fvar id a => mkApp2 (mkConst ``Key.fvar) (toExpr id) (toExpr a)
-   | .lit l => mkApp (mkConst ``Key.lit) (toExpr l)
-   | .star => mkConst ``Key.star
-   | .other => mkConst ``Key.other
-   | .arrow => mkConst ``Key.arrow
-   | .proj n i a => mkApp3 (mkConst ``Key.proj) (toExpr n) (toExpr i) (toExpr a)
-
 /--
 Discrimination tree trie. See `DiscrTree`.
 -/

src/Lean/Meta/DiscrTree/Util.lean

@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+prelude
+public import Lean.Meta.DiscrTree.Basic
+public section
+namespace Lean.Meta.DiscrTree
+namespace Trie
+/--
+Monadically fold the keys and values stored in a `Trie`.
+-/
+partial def foldM [Monad m] (initialKeys : Array Key)
+    (f : σ → Array Key → α → m σ) : (init : σ) → Trie α → m σ
+  | init, Trie.node vs children => do
+    let s ← vs.foldlM (init := init) fun s v => f s initialKeys v
+    children.foldlM (init := s) fun s (k, t) =>
+      t.foldM (initialKeys.push k) f s
+
+/--
+Fold the keys and values stored in a `Trie`.
+-/
+@[inline]
+def fold (initialKeys : Array Key) (f : σ → Array Key → α → σ) (init : σ) (t : Trie α) : σ :=
+  Id.run <| t.foldM initialKeys (init := init) fun s k a => return f s k a
+
+/--
+Monadically fold the values stored in a `Trie`.
+-/
+partial def foldValuesM [Monad m] (f : σ → α → m σ) : (init : σ) → Trie α → m σ
+  | init, node vs children => do
+    let s ← vs.foldlM (init := init) f
+    children.foldlM (init := s) fun s (_, c) => c.foldValuesM (init := s) f
+
+/--
+Fold the values stored in a `Trie`.
+-/
+@[inline]
+def foldValues (f : σ → α → σ) (init : σ) (t : Trie α) : σ :=
+  Id.run <| t.foldValuesM (init := init) (pure <| f · ·)
+
+/--
+The number of values stored in a `Trie`.
+-/
+partial def size : Trie α → Nat
+  | Trie.node vs children =>
+    children.foldl (init := vs.size) fun n (_, c) => n + size c
+
+end Trie
+
+
+/--
+Monadically fold over the keys and values stored in a `DiscrTree`.
+-/
+@[inline]
+def foldM [Monad m] (f : σ → Array Key → α → m σ) (init : σ)
+    (t : DiscrTree α) : m σ :=
+  t.root.foldlM (init := init) fun s k t => t.foldM #[k] (init := s) f
+
+/--
+Fold over the keys and values stored in a `DiscrTree`
+-/
+@[inline]
+def fold (f : σ → Array Key → α → σ) (init : σ) (t : DiscrTree α) : σ :=
+  Id.run <| t.foldM (init := init) fun s keys a => return f s keys a
+
+/--
+Monadically fold over the values stored in a `DiscrTree`.
+-/
+@[inline]
+def foldValuesM [Monad m] (f : σ → α → m σ) (init : σ) (t : DiscrTree α) :
+    m σ :=
+  t.root.foldlM (init := init) fun s _ t => t.foldValuesM (init := s) f
+
+/--
+Fold over the values stored in a `DiscrTree`.
+-/
+@[inline]
+def foldValues (f : σ → α → σ) (init : σ) (t : DiscrTree α) : σ :=
+  Id.run <| t.foldValuesM (init := init) (pure <| f · ·)
+
+/--
+Check for the presence of a value satisfying a predicate.
+-/
+@[inline]
+def containsValueP (t : DiscrTree α) (f : α → Bool) : Bool :=
+  t.foldValues (init := false) fun r a => r || f a
+
+/--
+Extract the values stored in a `DiscrTree`.
+-/
+@[inline]
+def values (t : DiscrTree α) : Array α :=
+  t.foldValues (init := #[]) fun as a => as.push a
+
+/--
+Extract the keys and values stored in a `DiscrTree`.
+-/
+@[inline]
+def toArray (t : DiscrTree α) : Array (Array Key × α) :=
+  t.fold (init := #[]) fun as keys a => as.push (keys, a)
+
+/--
+Get the number of values stored in a `DiscrTree`. O(n) in the size of the tree.
+-/
+@[inline]
+def size (t : DiscrTree α) : Nat :=
+  t.root.foldl (init := 0) fun n _ t => n + t.size
+
+variable {m : Type → Type} [Monad m]
+
+/-- Apply a monadic function to the array of values at each node in a `DiscrTree`. -/
+partial def Trie.mapArraysM (t : DiscrTree.Trie α) (f : Array α → m (Array β)) :
+    m (DiscrTree.Trie β) :=
+  match t with
+  | .node vs children =>
+    return .node (← f vs) (← children.mapM fun (k, t') => do pure (k, ← t'.mapArraysM f))
+
+/-- Apply a monadic function to the array of values at each node in a `DiscrTree`. -/
+def mapArraysM (d : DiscrTree α) (f : Array α → m (Array β)) : m (DiscrTree β) := do
+  pure { root := ← d.root.mapM (fun t => t.mapArraysM f) }
+
+/-- Apply a function to the array of values at each node in a `DiscrTree`. -/
+def mapArrays (d : DiscrTree α) (f : Array α → Array β) : DiscrTree β :=
+  Id.run <| d.mapArraysM fun A => pure (f A)
+
+end Lean.Meta.DiscrTree

src/Lean/Meta/ExprDefEq.lean

@@ -4,13 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.UnificationHint
 public import Lean.Util.OccursCheck
-
+import Lean.Meta.WHNF
 public section
-
 namespace Lean.Meta
 
 register_builtin_option backward.isDefEq.lazyProjDelta : Bool := {
@@ -374,7 +372,7 @@ private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr)
   isDefEqBindingAux lctx #[] a b #[]
 
 private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
-  withTraceNodeBefore `Meta.isDefEq.assign.checkTypes (return m!"({mvar} : {← inferType mvar}) := ({v} : {← inferType v})") do
+  withTraceNodeBefore `Meta.isDefEq.assign.checkTypes (fun _ => return m!"({mvar} : {← inferType mvar}) := ({v} : {← inferType v})") do
     if !mvar.isMVar then
       trace[Meta.isDefEq.assign.checkTypes] "metavariable expected"
       return false
@@ -1183,7 +1181,7 @@ private partial def processConstApprox (mvar : Expr) (args : Array Expr) (patter
 /-- Tries to solve `?m a₁ ... aₙ =?= v` by assigning `?m`.
     It assumes `?m` is unassigned. -/
 private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :=
-  withTraceNodeBefore `Meta.isDefEq.assign (return m!"{mvarApp} := {v}") do
+  withTraceNodeBefore `Meta.isDefEq.assign (fun _ => return m!"{mvarApp} := {v}") do
     let mvar := mvarApp.getAppFn
     let mvarDecl ← mvar.mvarId!.getDecl
     let rec process (i : Nat) (args : Array Expr) (v : Expr) := do
@@ -1338,7 +1336,7 @@ private def tryHeuristic (t s : Expr) : MetaM Bool := do
   unless (← isNonTrivialRegular info) || isMatcherCore (← getEnv) tFn.constName! do
     unless t.hasExprMVar || s.hasExprMVar do
       return false
-  withTraceNodeBefore `Meta.isDefEq.delta (return m!"{t} =?= {s}") do
+  withTraceNodeBefore `Meta.isDefEq.delta (fun _ => return m!"{t} =?= {s}") do
     recordDefEqHeuristic tFn.constName!
     /-
       We process arguments before universe levels to reduce a source of brittleness in the TC procedure.
@@ -1857,7 +1855,7 @@ end
   | none   => failK
 
 private def isDefEqOnFailure (t s : Expr) : MetaM Bool := do
-  withTraceNodeBefore `Meta.isDefEq.onFailure (return m!"{t} =?= {s}") do
+  withTraceNodeBefore `Meta.isDefEq.onFailure (fun _ => return m!"{t} =?= {s}") do
     unstuckMVar t (fun t => Meta.isExprDefEqAux t s) <|
     unstuckMVar s (fun s => Meta.isExprDefEqAux t s) <|
     tryUnificationHints t s <||> tryUnificationHints s t
@@ -2108,7 +2106,7 @@ private def whnfCoreAtDefEq (e : Expr) : MetaM Expr := do
 
 @[export lean_is_expr_def_eq]
 partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecDepth do
-  withTraceNodeBefore `Meta.isDefEq (return m!"{t} =?= {s}") do
+  withTraceNodeBefore `Meta.isDefEq (fun _ => return m!"{t} =?= {s}") do
   checkSystem "isDefEq"
   whenUndefDo (isDefEqQuick t s) do
   whenUndefDo (isDefEqProofIrrel t s) do

src/Lean/Meta/GetUnfoldableConst.lean

@@ -4,17 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.GlobalInstances
-
 public section
-
 namespace Lean.Meta
 
 private def canUnfoldDefault (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
   match cfg.transparency with
-  | .all => return true
+  | .none => return false
+  | .all  => return true
   | .default => return !(← isIrreducible info.name)
   | m =>
     if (← isReducible info.name) then

src/Lean/Meta/InferType.lean

@@ -178,7 +178,7 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do
   | none   => fvarId.throwUnknown
 
 @[inline] private def checkInferTypeCache (e : Expr) (inferType : MetaM Expr) : MetaM Expr := do
-  if e.hasMVar then
+  if !(← read).cacheInferType || e.hasMVar then
     inferType
   else
     let key ← mkExprConfigCacheKey e

src/Lean/Meta/Instances.lean

@@ -4,14 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Data.Range.Polymorphic.Stream
-public import Lean.Meta.DiscrTree
+public import Lean.Meta.DiscrTree.Main
 public import Lean.Meta.CollectMVars
-
+import Lean.Meta.WHNF
 public section
-
 namespace Lean.Meta
 
 register_builtin_option synthInstance.checkSynthOrder : Bool := {
@@ -77,8 +75,8 @@ structure Instances where
 
 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 }
-  | none   => { d with discrTree := d.discrTree.insertCore e.keys e }
+  | some n => { d with discrTree := d.discrTree.insertKeyValue e.keys e, instanceNames := d.instanceNames.insert n e, erased := d.erased.erase n }
+  | none   => { d with discrTree := d.discrTree.insertKeyValue e.keys e }
 
 def Instances.eraseCore (d : Instances) (declName : Name) : Instances :=
   { d with erased := d.erased.insert declName, instanceNames := d.instanceNames.erase declName }

src/Lean/Meta/Match/NamedPatterns.lean

@@ -4,15 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
-
+import Lean.Meta.Transform
+import Lean.Meta.WHNF
 /-!
 Helper functions around named patterns
 -/
-
 namespace Lean.Meta.Match
 
 public def mkNamedPattern (x h p : Expr) : MetaM Expr :=
@@ -36,3 +35,5 @@ public def unfoldNamedPattern (e : Expr) : MetaM Expr := do
         return TransformStep.visit eNew
     return .continue
   Meta.transform e (pre := visit)
+
+end Lean.Meta.Match

src/Lean/Meta/MethodSpecs.lean

@@ -3,12 +3,11 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joachim Breitner
 -/
-
 module
 prelude
 public import Lean.Meta.Tactic.Simp.SimpTheorems
 import Lean.Meta.Tactic.Simp.Main
-
+import Lean.Structure
 namespace Lean
 
 open Meta

src/Lean/Meta/SizeOf.lean

@@ -8,6 +8,7 @@ prelude
 public import Lean.AddDecl
 public import Lean.Meta.AppBuilder
 public import Lean.DefEqAttrib
+import Lean.Meta.WHNF
 public section
 namespace Lean.Meta
 

src/Lean/Meta/Structure.lean

@@ -4,19 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Kyle Miller
 -/
 module
-
 prelude
 public import Lean.AddDecl
 public import Lean.Meta.AppBuilder
-
+import Lean.Structure
+import Lean.Meta.Transform
 public section
-
+namespace Lean.Meta
 /-!
 # Structure methods that require `MetaM` infrastructure
 -/
 
-namespace Lean.Meta
-
 /--
 If `struct` is an application of the form `S ..` with `S` a constant for a structure,
 returns the name of the structure, otherwise throws an error.

src/Lean/Meta/Sym.lean

@@ -5,10 +5,24 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
+public import Lean.Meta.Sym.AlphaShareBuilder
+public import Lean.Meta.Sym.AlphaShareCommon
+public import Lean.Meta.Sym.ExprPtr
 public import Lean.Meta.Sym.SymM
-public import Lean.Meta.Sym.Main
-public import Lean.Meta.Sym.Util
 public import Lean.Meta.Sym.MaxFVar
+public import Lean.Meta.Sym.ReplaceS
+public import Lean.Meta.Sym.LooseBVarsS
+public import Lean.Meta.Sym.InstantiateS
+public import Lean.Meta.Sym.IsClass
+public import Lean.Meta.Sym.Intro
+public import Lean.Meta.Sym.InstantiateMVarsS
+public import Lean.Meta.Sym.ProofInstInfo
+public import Lean.Meta.Sym.AbstractS
+public import Lean.Meta.Sym.Pattern
+public import Lean.Meta.Sym.Apply
+public import Lean.Meta.Sym.InferType
+public import Lean.Meta.Sym.Simp
+public import Lean.Meta.Sym.Util
 
 /-!
 # Symbolic simulation support.
@@ -45,9 +59,47 @@ of `lctx₂`, we only need to verify that `lctx₂` contains the maximal free va
 means `x` is the free variable with maximal index occurring in `e`. When assigning `?m := e`, we check
 whether `maxFVar[e]` is in `?m.lctx` — a single hash lookup, O(1).
 
-**Maintaining `maxFVar`:** The mapping is updated during `intro`. The default `intro` in `MetaM` uses
-`instantiate` to replace `Expr.bvar` with `Expr.fvar`, using `looseBVarRange` to skip subexpressions
-without relevant bound variables. The `SymM` version piggybacks on this traversal to update `maxFVar`.
+**Maintaining `maxFVar`:** The mapping is automatically updated when we use `getMaxFVar?`.
+
+### Structural matching and definitional equality
+
+**The problem:** The `isDefEq` predicate in `MetaM` is designed for elaboration and user-facing tactics.
+It supports reduction, type-class resolution, and many other features that can be expensive or have
+unpredictable running time. For symbolic simulation, where pattern matching is called frequently on
+large ground terms, these features become performance bottlenecks.
+
+**The solution:** In `SymM`, pattern matching and definitional equality are restricted to a more syntactic,
+predictable subset. Key design choices:
+
+1. **Reducible declarations are abbreviations.** Reducible declarations are eagerly expanded when indexing
+   terms and when entering symbolic simulation mode. During matching, we assume abbreviations have already
+   been expanded.
+
+  **Why `MetaM` `simp` cannot make this assumption**: The simplifier in `MetaM` is designed for interactive use,
+  where users want to preserve their abstractions. Even reducible definitions may represent meaningful
+  abstractions that users may not want unfolded. For example, when applying `simp` to `x ≥ y`, users
+  typically do not want it transformed to `y ≤ x` just because `GE.ge` is a reducible abbreviation.
+
+2. **Proofs are ignored.** We skip proof arguments during matching due to proof irrelevance. Proofs are
+   "noisy": they are typically built using different automation or manually, so we can have radically
+   different proof terms for the same trivial fact.
+
+3. **Instances are ignored.** Lean's class hierarchy contains many diamonds. For example, `Add Nat` can be
+   obtained directly from the `Nat` library or derived from the fact that `Nat` is a `Semiring`. Proof
+   automation like `grind` attempts to canonicalize instances, but this is expensive. Instead, we treat
+   instances as support terms and skip them during matching, and we check them later using the standard
+   definitionally equality test in a mode where only reducible and instance declarations are unfolded.
+
+   **The implicit assumption:** If two terms have the same instance type, they are definitionally equal.
+   This holds in well-designed Lean code. For example, the `Add Nat` instance from the `Nat` library is
+   definitionally equal to the one derived from `Semiring`, and this can be established by unfolding only
+   reducible and instance declarations. Code that violates this assumption is considered misuse of Lean's
+   instance system.
+
+4. **Types must be indexed.** Unlike proofs and instances, types cannot be ignored, without indexing them,
+   pattern matching produces too many candidates. Like other abbreviations, type abbreviations are expanded.
+   Note that given `def Foo : Type := Bla`, the terms `Foo` and `Bla` are *not* considered structurally
+   equal in the symbolic simulator framework.
 
 ### Skipping type checks on assignment
 
@@ -63,17 +115,6 @@ Checks are also skipped when nothing new can be learned from them assuming terms
 For domain-specific constructors (e.g., `Exec.seq` in symbolic execution), types are typically ground,
 so the check is almost always skipped.
 
-### A syntactic definitional equality test
-
-**The problem:** The `isDefEq` predicate in `MetaM` is optimized for elaboration and user-facing tactics.
-It supports reduction, type-class resolution, and many other features that can be expensive or have
-unpredictable running time. For symbolic simulation, where `isDefEq` is called frequently, this can
-cause unexpected slowdowns.
-
-**The solution:** In `SymM`, the definitional equality test is optimized for the syntactic case. It avoids
-expensive steps such as lazy-delta reduction. Reduction rules such as `beta` are implemented with term
-size and algorithmic complexity in mind, ensuring predictable performance.
-
 ### `GrindM` state
 
 **The problem:** In symbolic simulation, we often want to discharge many goals using proof automation such

src/Lean/Meta/Sym/AbstractS.lean

@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.SymM
+import Lean.Meta.Sym.ReplaceS
+namespace Lean.Meta.Sym
+open Internal
+
+/--
+Helper function for implementing `abstractFVars` (and possible variants in the future).
+-/
+@[inline] def abstractFVarsCore (e : Expr) (lctx : LocalContext)
+    (maxFVar : PHashMap ExprPtr (Option FVarId))
+    (minFVarId : FVarId) (toDeBruijn? : FVarId → Option Nat) : AlphaShareBuilderM Expr := do
+  let minIndex := (lctx.find? minFVarId).get!.index
+  replaceS' e fun e offset => do
+    match e with
+    | .fvar fvarId =>
+      if let some bidx := toDeBruijn? fvarId then
+        mkBVarS (offset + bidx)
+      else
+        return some e
+    | .lit _ | .mvar _ | .bvar _ | .const _ _ | .sort _ =>
+      /-
+      Avoid `e.hasFVar` check.
+      **Note**: metavariables are safe to skip because we assume their local contexts never include
+      the free variables being abstracted (they were created before entering binders).
+      -/
+      return some e
+    | _ =>
+      -- Non-atomic expressions.
+      if !e.hasFVar then
+        -- Stop visiting: `e` does not contain free variables.
+        return some e
+      let some maxFVarId? := maxFVar.find? ⟨e⟩
+        | return none -- maxFVar information is not available, keep visiting
+      let maxIndex := (lctx.find? maxFVarId?.get!).get!.index
+      if maxIndex < minIndex then
+        -- Stop visiting: maximal free variable in `e` is smaller than minimal free variable being abstracted.
+        return some e
+      else
+        -- Keep visiting
+        return none
+
+/--
+Abstracts free variables `xs[start...*]` in expression `e`, converting them to de Bruijn indices.
+
+Assumptions:
+- The local context of the metavariables occurring in `e` do not include the free variables being
+  abstracted. This invariant holds when abstracting over binders during pattern matching/unification:
+  metavariables in the pattern were created before entering the binder, so their contexts exclude
+  the bound variable's corresponding fvar.
+
+- If `xs[start...*]` is not empty, then the minimal variable is `xs[start]`.
+
+- Subterms whose `maxFVar` is below `minFVarId` are skipped entirely. This function does not assume
+the `maxFVar` cache contains information for every subterm in `e`.
+-/
+public def abstractFVarsRange (e : Expr) (start : Nat) (xs : Array Expr) : SymM Expr := do
+  if !e.hasFVar then return e
+  if h : start < xs.size then
+    let toDeBruijn? (fvarId : FVarId) : Option Nat :=
+      let rec go (bidx : Nat) (i : Nat) (h : i < xs.size) : Option Nat :=
+        if xs[i].fvarId! == fvarId then
+          some bidx
+        else if i > start then
+          go (bidx + 1) (i - 1) (by omega)
+        else
+          none
+      go 0 (xs.size - 1) (by omega)
+    liftBuilderM <| abstractFVarsCore e (← getLCtx) (← get).maxFVar xs[start].fvarId! toDeBruijn?
+  else
+    return e
+
+/--
+Abstracts free variables `xs` in expression `e`, converting them to de Bruijn indices.
+
+It is an abbreviation for `abstractFVarsRange e 0 xs`.
+-/
+public abbrev abstractFVars (e : Expr) (xs : Array Expr) : SymM Expr := do
+  abstractFVarsRange e 0 xs
+
+/--
+Similar to `mkLambdaFVars`, but uses the more efficient `abstractFVars` and `abstractFVarsRange`,
+and makes the same assumption made by these functions.
+-/
+public def mkLambdaFVarsS (xs : Array Expr) (e : Expr) : SymM Expr := do
+  let b ← abstractFVars e xs
+  xs.size.foldRevM (init := b) fun i _ b => do
+    let x := xs[i]
+    let decl ← x.fvarId!.getDecl
+    let type ← abstractFVarsRange decl.type i xs
+    mkLambdaS decl.userName decl.binderInfo type b
+
+end Lean.Meta.Sym

src/Lean/Meta/Sym/AlphaShareBuilder.lean

@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.SymM
+public section
+namespace Lean.Meta.Sym.Internal
+/-!
+Helper functions for constructing maximally shared expressions from maximally shared expressions.
+That is, `mkAppS f a` assumes that `f` and `a` are maximally shared.
+
+These functions are in the `Internal` namespace because they can be easily misused.
+We use them to construct safe functions.
+-/
+class MonadShareCommon (m : Type → Type) where
+  share1 : Expr → m Expr
+  assertShared : Expr → m Unit
+  isDebugEnabled : m Bool
+
+@[always_inline]
+instance (m n) [MonadLift m n] [MonadShareCommon m] : MonadShareCommon n where
+  share1 e := liftM (MonadShareCommon.share1 e : m Expr)
+  assertShared e := liftM (MonadShareCommon.assertShared e : m Unit)
+  isDebugEnabled := liftM (MonadShareCommon.isDebugEnabled : m Bool)
+
+private def dummy : AlphaKey := { expr := mkConst `__dummy__}
+
+protected def Sym.share1 (e : Expr) : SymM Expr := do
+  let prev := (← get).share.set.findD { expr := e } dummy
+  if isSameExpr prev.expr dummy.expr then
+    -- `e` is new
+    modify fun s => { s with share.set := s.share.set.insert { expr := e } }
+    return e
+  else
+    return prev.expr
+
+protected def Sym.assertShared (e : Expr) : SymM Unit := do
+  let prev := (← get).share.set.findD { expr := e } dummy
+  assert! isSameExpr prev.expr e
+
+instance : MonadShareCommon SymM where
+  share1 := Sym.share1
+  assertShared := Sym.assertShared
+  isDebugEnabled := isDebugEnabled
+
+/--
+Helper monad for constructing maximally shared terms.
+The `Bool` flag indicates whether it is debug-mode or not.
+-/
+abbrev AlphaShareBuilderM := ReaderT Bool AlphaShareCommonM
+
+/--
+Helper function for lifting a `AlphaShareBuilderM` action to `GrindM`
+-/
+abbrev liftBuilderM (k : AlphaShareBuilderM α) : SymM α := do
+  let share ← modifyGet fun s => (s.share, { s with share := {} })
+  let (a, share) := k (← isDebugEnabled) share
+  modify fun s => { s with share }
+  return a
+
+protected def Builder.share1 (e : Expr) : AlphaShareBuilderM Expr := do
+  let prev := (← get).set.findD { expr := e } dummy
+  if isSameExpr prev.expr dummy.expr then
+    -- `e` is new
+    modify fun { set := set } => { set := set.insert { expr := e } }
+    return e
+  else
+    return prev.expr
+
+protected def Builder.assertShared (e : Expr) : AlphaShareBuilderM Unit := do
+  assert! (← get).set.contains ⟨e⟩
+
+instance : MonadShareCommon AlphaShareBuilderM where
+  share1 := Builder.share1
+  assertShared := Builder.assertShared
+  isDebugEnabled := read
+
+open MonadShareCommon (share1 assertShared)
+
+variable [MonadShareCommon m]
+
+def mkLitS (l : Literal) : m Expr :=
+  share1 <| .lit l
+
+def mkConstS (declName : Name) (us : List Level := []) : m Expr :=
+  share1 <| .const declName us
+
+def mkBVarS (idx : Nat) : m Expr :=
+  share1 <| .bvar idx
+
+def mkSortS (u : Level) : m Expr :=
+  share1 <| .sort u
+
+def mkFVarS (fvarId : FVarId) : m Expr :=
+  share1 <| .fvar fvarId
+
+def mkMVarS (mvarId : MVarId) : m Expr :=
+  share1 <| .mvar mvarId
+
+variable [Monad m]
+
+def mkMDataS (d : MData) (e : Expr) : m Expr := do
+  if (← MonadShareCommon.isDebugEnabled) then
+    assertShared e
+  share1 <| .mdata d e
+
+def mkProjS (structName : Name) (idx : Nat) (struct : Expr) : m Expr := do
+  if (← MonadShareCommon.isDebugEnabled) then
+    assertShared struct
+  share1 <| .proj structName idx struct
+
+def mkAppS (f a : Expr) : m Expr := do
+  if (← MonadShareCommon.isDebugEnabled) then
+    assertShared f
+    assertShared a
+  share1 <| .app f a
+
+def mkLambdaS (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : m Expr := do
+  if (← MonadShareCommon.isDebugEnabled) then
+    assertShared t
+    assertShared b
+  share1 <| .lam x t b bi
+
+def mkForallS (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : m Expr := do
+  if (← MonadShareCommon.isDebugEnabled) then
+    assertShared t
+    assertShared b
+  share1 <| .forallE x t b bi
+
+def mkLetS (x : Name) (t : Expr) (v : Expr) (b : Expr) (nondep : Bool := false) : m Expr := do
+  if (← MonadShareCommon.isDebugEnabled) then
+    assertShared t
+    assertShared v
+    assertShared b
+  share1 <| .letE x t v b nondep
+
+def mkHaveS (x : Name) (t : Expr) (v : Expr) (b : Expr) : m Expr := do
+  if (← MonadShareCommon.isDebugEnabled) then
+    assertShared t
+    assertShared v
+    assertShared b
+  share1 <| .letE x t v b true
+
+end Lean.Meta.Sym.Internal

src/Lean/Meta/Sym/AlphaShareCommon.lean

@@ -0,0 +1,183 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.ExprPtr
+public section
+namespace Lean.Meta.Sym
+
+private def hashChild (e : Expr) : UInt64 :=
+  match e with
+  | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. =>
+    hash e
+  | .app .. | .letE .. | .forallE .. | .lam .. | .mdata .. | .proj .. =>
+    hashPtrExpr e
+
+private def alphaHash (e : Expr) : UInt64 :=
+  match e with
+  | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. =>
+    hash e
+  | .app f a => mixHash (hashChild f) (hashChild a)
+  | .letE _ _ v b _ => mixHash (hashChild v) (hashChild b)
+  | .forallE _ d b _ | .lam _ d b _ => mixHash (hashChild d) (hashChild b)
+  | .mdata _ b => mixHash 13 (hashChild b)
+  | .proj n i b => mixHash (mixHash (hash n) (hash i)) (hashChild b)
+
+private def alphaEq (e₁ e₂ : Expr) : Bool := Id.run do
+  match e₁ with
+  | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. =>
+    e₁ == e₂
+  | .app f₁ a₁ =>
+    let .app f₂ a₂ := e₂ | false
+    isSameExpr f₁ f₂ && isSameExpr a₁ a₂
+  | .letE _ _ v₁ b₁ _ =>
+    let .letE _ _ v₂ b₂ _ := e₂ | false
+    isSameExpr v₁ v₂ && isSameExpr b₁ b₂
+  | .forallE _ d₁ b₁ _ =>
+    let .forallE _ d₂ b₂ _ := e₂ | false
+    isSameExpr d₁ d₂ && isSameExpr b₁ b₂
+  | .lam _ d₁ b₁ _ =>
+    let .lam _ d₂ b₂ _ := e₂ | false
+    isSameExpr d₁ d₂ && isSameExpr b₁ b₂
+  | .mdata d₁ b₁ =>
+    let .mdata d₂ b₂ := e₂ | false
+    return isSameExpr b₁ b₂ && d₁ == d₂
+  | .proj n₁ i₁ b₁ =>
+    let .proj n₂ i₂ b₂ := e₂ | false
+    n₁ == n₂ && i₁ == i₂ && isSameExpr b₁ b₂
+
+structure AlphaKey where
+  expr : Expr
+
+instance : Hashable AlphaKey where
+  hash k := private alphaHash k.expr
+
+instance : BEq AlphaKey where
+  beq k₁ k₂ := private alphaEq k₁.expr k₂.expr
+
+structure AlphaShareCommon.State where
+  set : PHashSet AlphaKey := {}
+
+abbrev AlphaShareCommonM := StateM AlphaShareCommon.State
+
+private structure State where
+  map : Std.HashMap ExprPtr Expr := {}
+  set : PHashSet AlphaKey := {}
+
+private abbrev M := StateM State
+
+private def dummy : AlphaKey := { expr := mkConst `__dummy__}
+
+private def save (e : Expr) (r : Expr) : M Expr := do
+  let prev := (← get).set.findD { expr := r } dummy
+  if isSameExpr prev.expr dummy.expr then
+    -- `r` is new
+    modify fun { set, map } => {
+      set := set.insert { expr := r }
+      map := map.insert { expr := e } r |>.insert { expr := r } r
+    }
+    return r
+  else
+    let r := prev.expr
+    modify fun { set, map } => {
+      set
+      map := map.insert { expr := e } r
+    }
+    return r
+
+private abbrev visit (e : Expr) (k : M Expr) : M Expr := do
+  /-
+  **Note**: The input may be a DAG, and we don't want to visit the same sub-expression
+  over and over again.
+  -/
+  if let some r := (← get).map[{ expr := e : ExprPtr }]? then
+    return r
+  else
+  /-
+  **Note**: The input may contain sub-expressions that have already been processed and are
+  already maximally shared.
+  -/
+  let prev := (← get).set.findD { expr := e } dummy
+  if isSameExpr prev.expr dummy.expr then
+    -- `e` has not been hash-consed before
+    save e (← k)
+  else
+    return prev.expr
+
+private def go (e : Expr) : M Expr := do
+  match e with
+  | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. =>
+    if let some r := (← get).set.find? { expr := e } then
+      return r.expr
+    else
+      modify fun { set, map } => { set := set.insert { expr := e }, map }
+      return e
+  | .app f a => visit e (return e.updateApp! (← go f) (← go a))
+  | .letE _ t v b _ => visit e (return e.updateLetE! (← go t) (← go v) (← go b))
+  | .forallE _ d b _ => visit e (return e.updateForallE! (← go d) (← go b))
+  | .lam _ d b _ => visit e (return e.updateLambdaE! (← go d) (← go b))
+  | .mdata _ b => visit e (return e.updateMData! (← go b))
+  | .proj _ _ b => visit e (return e.updateProj! (← go b))
+
+/-- Similar to `shareCommon`, but handles alpha-equivalence. -/
+@[inline] def shareCommonAlpha (e : Expr) : AlphaShareCommonM Expr := fun s =>
+  if let some r := s.set.find? { expr := e } then
+    (r.expr, s)
+  else
+    let (e, { set, .. }) := go e |>.run { map := {}, set := s.set }
+    (e, ⟨set⟩)
+
+private def saveInc (e : Expr) : AlphaShareCommonM Expr := do
+  let prev := (← get).set.findD { expr := e } dummy
+  if isSameExpr prev.expr dummy.expr then
+    -- `e` is new
+    modify fun { set := set } => { set := set.insert { expr := e } }
+    return e
+  else
+    return prev.expr
+
+@[inline] private def visitInc (e : Expr) (k : AlphaShareCommonM Expr) : AlphaShareCommonM Expr := do
+  let prev := (← get).set.findD { expr := e } dummy
+  if isSameExpr prev.expr dummy.expr then
+    -- `e` has now been cached before
+    saveInc (← k)
+  else
+    return prev.expr
+
+/--
+Incremental variant of `shareCommonAlpha` for expressions constructed from already-shared subterms.
+
+Use this when an expression `e` was produced by a Lean API (e.g., `inferType`, `mkApp4`) that
+does not preserve maximal sharing, but the inputs to that API were already maximally shared.
+In this case, only the newly constructed nodes need processing—the shared subterms can be
+looked up directly in the `AlphaShareCommonM` state without building a temporary hashmap.
+
+Unlike `shareCommonAlpha`, this function does not use a local `Std.HashMap ExprPtr Expr` to
+track visited nodes. This is more efficient when the number of new (unshared) nodes is small,
+which is the common case when wrapping API calls that build a few constructor nodes around
+shared inputs.
+
+Example:
+```
+-- `a` and `b` are already maximally shared
+let result := mkApp2 f a b  -- result is not maximally shared
+let result ← shareCommonAlphaInc result -- efficiently restore sharing
+```
+-/
+@[inline] def shareCommonAlphaInc (e : Expr) : AlphaShareCommonM Expr :=
+  go e
+where
+  go (e : Expr) : AlphaShareCommonM Expr := do
+  match e with
+  | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. => saveInc e
+  | .app f a => visitInc e (return e.updateApp! (← go f) (← go a))
+  | .letE _ t v b _ => visitInc e (return e.updateLetE! (← go t) (← go v) (← go b))
+  | .forallE _ d b _ => visitInc e (return e.updateForallE! (← go d) (← go b))
+  | .lam _ d b _ => visitInc e (return e.updateLambdaE! (← go d) (← go b))
+  | .mdata _ b => visitInc e (return e.updateMData! (← go b))
+  | .proj _ _ b => visitInc e (return e.updateProj! (← go b))
+
+end Lean.Meta.Sym

src/Lean/Meta/Sym/Apply.lean

@@ -0,0 +1,117 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.Pattern
+import Lean.Util.CollectFVars
+namespace Lean.Meta.Sym
+
+/--
+A rule for backward chaining (goal transformation).
+
+Given a goal `... ⊢ T`, applying a `BackwardRule` derived from a theorem `∀ xs, P`
+will unify `T` with `P`, assign the goal to the theorem application,
+and return new goals for the unassigned arguments in `xs`.
+-/
+public structure BackwardRule where
+  /-- The theorem used to create the rule. It is often of the form `Expr.const declName`. -/
+  expr      : Expr
+  /-- Precomputed pattern for efficient unification. -/
+  pattern   : Pattern
+  /--
+  Indices of arguments that become new subgoals, ordered with
+  non-dependent goals first. -/
+  resultPos : List Nat
+
+
+/--
+Computes which argument positions become new subgoals after applying a backward rule.
+
+Arguments are excluded from `resultPos` if:
+- They appear in the conclusion (will be determined by unification)
+- They are instance arguments (will be synthesized)
+
+The result is ordered with non-dependent arguments first, then dependent ones.
+This ordering is the same one used for the `MetaM` `apply` tactic.
+It improves the user experience: non-dependent goals can be solved in
+any order, while dependent goals are often resolved by solving the non-dependent ones first.
+Example: `Exists.intro` produces two subgoal `?h : ?p ?w` and `?w : ?α`. The goal `?h` appears
+first because solving it often solves `?w`.
+-/
+def mkResultPos (pattern : Pattern) : List Nat := Id.run do
+  let auxPrefix := `_sym_pre
+  -- Initialize "found" mask with arguments that can be synthesized by type class resolution.
+  let mut found := pattern.isInstance
+  let numArgs := pattern.varTypes.size
+  let auxVars := pattern.varTypes.mapIdx fun i _ => mkFVar ⟨.num auxPrefix i⟩
+  -- Collect arguments that occur in the pattern
+  for fvarId in collectFVars {} (pattern.pattern.instantiateRev auxVars) |>.fvarIds do
+    let .num pre idx := fvarId.name | pure ()
+    if pre == auxPrefix then
+      found := found.set! idx true
+  let argTypes := pattern.varTypes.mapIdx fun i type => type.instantiateRevRange 0 i auxVars
+  -- Collect dependent and non-dependent arguments that become new goals
+  -- An argument is considered dependent only if there is another goal whose type depends on it.
+  let mut deps := #[]
+  let mut nonDeps := #[]
+  for i in *...numArgs do
+    unless found[i]! do
+      let auxVar := auxVars[i]!
+      let mut isDep := false
+      for j in (i+1)...numArgs do
+        unless found[j]! do
+          let argType := argTypes[j]!
+          if argType.containsFVar auxVar.fvarId! then
+            isDep := true
+            break
+      if isDep then
+        deps := deps.push i
+      else
+        nonDeps := nonDeps.push i
+  return (nonDeps ++ deps).toList
+
+/--
+Creates a `BackwardRule` from a declaration name.
+
+The `num?` parameter optionally limits how many arguments are included in the pattern
+(useful for partially applying theorems).
+-/
+public def mkBackwardRuleFromDecl (declName : Name) (num? : Option Nat := none) : MetaM BackwardRule := do
+  let pattern ← mkPatternFromDecl declName num?
+  let resultPos := mkResultPos pattern
+  return { expr := mkConst declName, pattern, resultPos }
+
+/--
+Creates a value to assign to input goal metavariable using unification result.
+
+Handles both constant expressions (common case, avoids `instantiateLevelParams`)
+and general expressions.
+-/
+def mkValue (expr : Expr) (pattern : Pattern) (result : MatchUnifyResult) : Expr :=
+  if let .const declName [] := expr then
+    mkAppN (mkConst declName result.us) result.args
+  else
+    mkAppN (expr.instantiateLevelParams pattern.levelParams result.us) result.args
+
+/--
+Applies a backward rule to a goal, returning new subgoals.
+
+1. Unifies the goal type with the rule's pattern
+2. Assigns the goal metavariable to the theorem application
+3. Returns new goals for unassigned arguments (per `resultPos`)
+
+Throws an error if unification fails.
+-/
+public def BackwardRule.apply (mvarId : MVarId) (rule : BackwardRule) : SymM (List MVarId) := mvarId.withContext do
+  let decl ← mvarId.getDecl
+  if let some result ← rule.pattern.unify? decl.type then
+    mvarId.assign (mkValue rule.expr rule.pattern result)
+    return rule.resultPos.map fun i =>
+      result.args[i]!.mvarId!
+  else
+    throwError "rule is not applicable to goal{mvarId}rule:{indentExpr rule.expr}"
+
+end Lean.Meta.Sym

src/Lean/Meta/Sym/ExprPtr.lean

@@ -7,7 +7,7 @@ module
 prelude
 public import Lean.Expr
 public section
-namespace Lean.Meta.Grind
+namespace Lean.Meta.Sym
 
 @[inline] def isSameExpr (a b : Expr) : Bool :=
   -- It is safe to use pointer equality because we hashcons all expressions
@@ -31,4 +31,4 @@ instance : Hashable ExprPtr where
 instance : BEq ExprPtr where
   beq k₁ k₂ := isSameExpr k₁.expr k₂.expr
 
-end Lean.Meta.Grind
+end Lean.Meta.Sym

src/Lean/Meta/Sym/InferType.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.SymM
+namespace Lean.Meta.Sym
+
+def inferTypeWithoutCache (e : Expr) : MetaM Expr :=
+  withReader (fun c => { c with cacheInferType := false }) do
+    Meta.inferType e
+
+def getLevelWithoutCache (type : Expr) : MetaM Level :=
+  withReader (fun c => { c with cacheInferType := false }) do
+    Meta.getLevel type
+
+/-- Returns the type of `e`. -/
+public def inferType (e : Expr) : SymM Expr := do
+  if let some type := (← get).inferType.find? { expr := e } then
+    return type
+  else
+    let type ← shareCommonInc (← inferTypeWithoutCache e)
+    modify fun s => { s with inferType := s.inferType.insert { expr := e } type }
+    return type
+
+@[inherit_doc Meta.getLevel]
+public def getLevel (type : Expr) : SymM Level := do
+  if let some u := (← get).getLevel.find? { expr := type } then
+    return u
+  else
+    let u ← getLevelWithoutCache type
+    modify fun s => { s with getLevel := s.getLevel.insert { expr := type } u }
+    return u
+
+public def mkEqRefl (e : Expr) : SymM Expr := do
+  let α ← inferType e
+  let u ← getLevel α
+  return mkApp2 (mkConst ``Eq.refl [u]) α e
+
+end Lean.Meta.Sym