max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: message context in grind code actions (#10473)

Browse source 
This PR ensures the code action messages produced by `grind` include the
full context
This commit is contained in:
Leonardo de Moura 2025-09-20 01:02:12 -07:00 • committed by GitHub
parent fc718eac88
commit 9b842b7554
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
View file

@ -1396,7 +1396,9 @@ def EMatchTheoremKind.toSyntax (kind : EMatchTheoremKind) : CoreM (TSyntax ``Par
private def save (ref : Syntax) (thm : EMatchTheorem) (isParam : Bool) (minIndexable : Bool) : SelectM Unit := do
-- We only save `thm` if the pattern is different from the ones that were already found.
if (← get).thms.all fun thm' => thm.patterns != thm'.patterns then
let pats ← thm.patterns.mapM fun p => (ppPattern p).toString
let pats ← thm.patterns.mapM fun p => do
let pats ← addMessageContextFull (ppPattern p)
pats.format
let openBracket := if isParam then "" else "["
let closeBracket := if isParam then "" else "]"
let msg := s!"{closeBracket} for pattern: {pats}"