Def Mathlib.Linter.UnusedTactic.initialAllowedUnusedTactics

Modification history

2026-10-20 18:25

Mathlib/Tactic/Linter/UnusedTactic.lean

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

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