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

chore: display E-matching theorems in goalToMessageData (#6635)

Browse source 
This PR includes the activated E-matching theorems and their patterns in
`goalToMessageData`
This commit is contained in:
Leonardo de Moura 2025-01-13 18:25:30 -08:00 • committed by GitHub
parent f57745e9d4
commit d6f0c324c3
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Meta/Tactic/Grind/PP.lean
View file

@ -99,10 +99,23 @@ private def ppEqcs (goal : Goal) : MetaM (Array MessageData) := do
result := result.push <| .trace { cls := `eqc } "Equivalence classes" otherEqcs
return result
private def ppEMatchTheorem (thm : EMatchTheorem) : MetaM MessageData := do
let m := m!"{← thm.origin.pp}\n{← inferType thm.proof}\npatterns: {thm.patterns.map ppPattern}"
return .trace { cls := `thm } m #[]
private def ppActiveTheorems (goal : Goal) : MetaM MessageData := do
let m ← goal.thms.toArray.mapM ppEMatchTheorem
let m := m ++ (← goal.newThms.toArray.mapM ppEMatchTheorem)
if m.isEmpty then
return ""
else
return .trace { cls := `ematch } "E-matching" m
def goalToMessageData (goal : Goal) : MetaM MessageData := goal.mvarId.withContext do
let mut m : Array MessageData := #[.ofGoal goal.mvarId]
m := m.push <| ppExprArray `facts "Asserted facts" goal.facts.toArray `prop
m := m ++ (← ppEqcs goal)
m := m.push (← ppActiveTheorems goal)
addMessageContextFull <| MessageData.joinSep m.toList ""
def goalsToMessageData (goals : List Goal) : MetaM MessageData :=