This file defines the environment extension to keep track of which tactics are allowed to leave the tactic state unchanged and not trigger the unused tactic linter.

opaque Mathlib.Linter.UnusedTactic.allowedUnusedTacticExt : Lean.SimplePersistentEnvExtension Lean.SyntaxNodeKind (Std.HashSet Lean.SyntaxNodeKind)

Defines the allowedUnusedTacticExt extension for adding a HashSet of allowedUnusedTactics to the environment.

def Mathlib.Linter.UnusedTactic.addAllowedUnusedTactic {m : Type → Type} [Monad m] [Lean.MonadEnv m] (stxNodes : Std.HashSet Lean.SyntaxNodeKind) : m Unit

addAllowedUnusedTactic stxNodes takes as input a HashSet of SyntaxNodeKinds and extends the allowedUnusedTacticExt environment extension with its content.

These are tactics that the unused tactic linter will ignore, since they are expected to not change the tactic state.

See the #allow_unused_tactic! ids command for dynamically extending the extension as a user-facing command.

Equations

• One or more equations did not get rendered due to their size.

opaque Mathlib.Linter.UnusedTactic.allowedRef : IO.Ref (Std.HashSet Lean.SyntaxNodeKind)

Parsers allowed to not change the tactic state. This can be increased dynamically, using #allow_unused_tactic.

def Mathlib.Linter.UnusedTactic.«command#allow_unused_tactic!___» : Lean.ParserDescr

#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

#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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Linter.UnusedTactic.«command#show_kind_» : Lean.ParserDescr

#show_kind tac takes as input the syntax of a tactic and returns the SyntaxNodeKind at the head of the tactic syntax tree.

The input syntax needs to parse, though it can be extremely elided. For instance, to see the SyntaxNodeKind of the refine tactic, you could use

#show_kind refine _

The trailing underscore _ makes the syntax valid, since refine expects something else.

Equations

• One or more equations did not get rendered due to their size.