Commit 2025-02-10 11:41 3d1c97d4
View on Github →feat: persistent #allow_unused_tactic (#20438)
Adds #allow_unused_tactic!, the persistent version of #allow_unused_tactic.
For instance, writing
#allow_unused_tactic!
Lean.Parser.Tactic.done
Lean.Parser.Tactic.skip
makes the tactics done and skip invisible to the unused tactic linter from where the command is issued onwards, also in files that transitively import the file where the command appears.
The PR also includes a utility function #show_kind tac to help find the SyntaxNodeKind of the tactic tac. For instance, using
#show_kind exact _
reports that the SyntaxNodeKind is 'Lean.Parser.Tactic.exact'..
Zulip