Def Mathlib.Linter.UnusedTactic.addAllowedUnusedTactic

Modification history

2026-10-20 18:25

Mathlib/Tactic/Linter/UnusedTactic.lean

fix(Linter/UnusedTactic): don't use `IO.Ref` for extensibility (#42536) …

Modified Mathlib.Linter.UnusedTactic.addAllowedUnusedTactic View on Github →

2025-02-10 11:41

Mathlib/Tactic/Linter/UnusedTacticExtension.lean

feat: persistent `#allow_unused_tactic` (#20438) …

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