Def Lean.Elab.ContextInfo.runTacticCodeCapturingInfoTree

Modification history

2026-02-17 05:26

Mathlib/Lean/ContextInfo.lean

feat(TacticAnalysis): verify grind? suggestions work (#33645) …

Added Lean.Elab.ContextInfo.runTacticCodeCapturingInfoTree View on Github →