add some explanation

leanprover · Feb 6, 2025 · 18c9e61 · 18c9e61
1 parent 56c9748
commit 18c9e61
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -195,6 +195,9 @@ structure SimpTheorems where
 
 /--
 Configuration for `MetaM` used to process global simp theorems
+
+Note that this configuration should be similar to the default `simp` configuration,
+so that the discrimination tree keys are appropriate for `simp`lified expressions.
 -/
 def simpGlobalConfig : ConfigWithKey :=
   { proj         := .no

diff --git a/tests/lean/run/6909.lean b/tests/lean/run/6909.lean
@@ -4,6 +4,13 @@ abbrev Multiseries : List Nat → Type
 
 opaque maxExp (n : Nat) (ns : List Nat) (li : List (Multiseries (n :: ns))) : Nat
 
+/-
+Previously, this lemma couldn't simplify itself, because the discrimination tree
+keys were computed with `iota := false`.
+Because `simp` uses `iota := true`, `Multiseries (n :: ns)` reduces to `Int`,
+so the discrimination tree keys didn't match.
+-/
+
 @[simp]
 axiom bad_simp_lemma (n : Nat) (ns : List Nat) : maxExp n ns [] = 8