Def Mathlib.TacticAnalysis.findTacticSeqs

Modification history

2026-10-05 12:25
Mathlib/Tactic/TacticAnalysis.lean
perf(TacticAnalysis): reimplement `findTacticSeqs` (#44445) …
Modified Mathlib.TacticAnalysis.findTacticSeqsView on Github →
2025-11-04 18:11
Mathlib/Tactic/TacticAnalysis.lean
feat(TacticAnalysis): check if we are in a `try`/`anyGoals` context (#29964) …
Modified Mathlib.TacticAnalysis.findTacticSeqsView on Github →
2025-10-31 10:48
Mathlib/Tactic/TacticAnalysis.lean
fix(TacticAnalysis): remove syntax range check (#28950) …
Modified Mathlib.TacticAnalysis.findTacticSeqsView on Github →
2025-08-14 23:22
Mathlib/Tactic/TacticAnalysis.lean
feat: tactic analysis framework (#26683) …
Added Mathlib.TacticAnalysis.findTacticSeqsView on Github →