Commit 2024-06-30 04:52 3415a86b

feat: unused tactic linter (#11308) The unusedTactic linter emits a warning if a tactic does nothing. Previous PRs (see below) removed all the "unused tactics" that the linter flagged. Here is an overview of this PR:

• the linter is defined in Mathlib/Tactic/Linter/UnusedTactic.lean;
• the file Mathlib/GroupTheory/Perm/Cycle/Concrete.lean contains the "only" set_option to opt out of the linter, since it defines notation that uses decide that the notation itself does not use;
• 17 test files that have surgically opted out of the linter;
• noise to import the new file, place it low in the import hierarchy and update noshake. PRs removing some unused tactics:
• #11333
• #11351
• #11365
• #11379 Zulip thread