Lean4
/-- `#allow_unused_tactic` takes as input a space-separated list of identifiers.
These identifiers are then allowed by the unused tactic linter:
even if these tactics do not modify goals, there will be no warning emitted.
Note: for this to work, these identifiers should be the `SyntaxNodeKind` of each tactic.
For instance, you can allow the `done` and `skip` tactics using
```lean
#allow_unused_tactic Lean.Parser.Tactic.done Lean.Parser.Tactic.skip
```
This change is file-local. If you want a *persistent* change, then use the `!`-flag:
the command `#allow_unused_tactic! ids` makes the change the linter continues to ignore these
tactics also in files importing a file where this command is issued.
The command `#show_kind tac` may help to find the `SyntaxNodeKind`.
-/
@[command_parser 1000]
public meta def «command#allow_unused_tactic!___» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Linter.UnusedTactic.«command#allow_unused_tactic!___» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "#allow_unused_tactic")
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "!")))
(ParserDescr.unary✝ `group (ParserDescr.const✝ `ppSpace)))
(ParserDescr.unary✝ `group (ParserDescr.const✝ `colGt)))
(ParserDescr.unary✝ `many (ParserDescr.const✝ `ident)))
