Def Lean.Elab.ContextInfo.runTacticCode

Modification history

2025-11-11 10:35
Mathlib/Lean/ContextInfo.lean
fix: panic in tactic analysis framework (#31472) …
Modified Lean.Elab.ContextInfo.runTacticCodeView on Github →
2025-09-11 00:51
Mathlib/Lean/ContextInfo.lean
fix(TacticAnalysis): include more `CommandElabM` state calling `runTactic` (#29505) …
Added Lean.Elab.ContextInfo.runTacticCodeView on Github →