Def terminalToGrind

Modification history

2025-10-31 08:48
Mathlib/Tactic/TacticAnalysis/Declarations.lean
feat: tryAtEachStep linters run on a fraction of goals (#31039) …
Deleted terminalToGrindView on Github →
2025-08-14 23:22
Mathlib/Tactic/TacticAnalysis/Declarations.lean
feat: tactic analysis framework (#26683) …
Added terminalToGrindView on Github →