Def Lean.Elab.ContextInfo.runCoreMWithMessages

Modification history

2025-08-14 23:22
Mathlib/Lean/ContextInfo.lean
feat: tactic analysis framework (#26683) …
Added Lean.Elab.ContextInfo.runCoreMWithMessagesView on Github →