Def Lean.Elab.ContextInfo.runTacticCapturingInfoTree

Modification history

2026-02-17 05:26

Mathlib/Lean/ContextInfo.lean

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

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