Def Mathlib.Linter.UnusedTactic.addIgnoreTacticKind

Modification history

2026-08-12 09:46

Mathlib/Tactic/Linter/UnusedTactic.lean

feat(Tactic/Linter/UnusedTactic): mark `isIgnoreTacticKind` and `addIgnoreTacticKind` as public (#41993) …

Deleted Mathlib.Linter.UnusedTactic.addIgnoreTacticKind View on Github →

2024-06-30 04:52

Mathlib/Tactic/Linter/UnusedTactic.lean

feat: unused tactic linter (#11308) …

Added Mathlib.Linter.UnusedTactic.addIgnoreTacticKind View on Github →