# Documentation

Std.Linter.UnreachableTactic

Enables the 'unreachable tactic' linter. This will warn on any tactics that are never executed. For example, in example : True := by trivial <;> done, the tactic done is never executed because trivial produces no subgoals; you could put sorry or apply I_don't_exist or anything else there and no error would result.

A common source of such things is simp <;> tac in the case that simp improves and closes a subgoal that was previously being closed by tac.

Gets the value of the linter.unreachableTactic option.

Equations
@[inline]

The monad for collecting used tactic syntaxes.

Equations

A list of blacklisted syntax kinds, which are expected to have subterms that contain unevaluated tactics.

Is this a syntax kind that contains intentionally unevaluated tactic subterms?

Equations

Adds a new syntax kind whose children will be ignored by the unreachableTactic linter. This should be called from an initialize block.

Equations
@[specialize #[]]
partial def Std.Linter.UnreachableTactic.getTactics (ignoreTacticKinds : Lean.NameHashSet) (isTacKind : ) (stx : Lean.Syntax) :

Accumulates the set of tactic syntaxes that should be evaluated at least once.

Search for tactic executions in the info tree and remove executed tactic syntaxes.

Search for tactic executions in the info tree and remove executed tactic syntaxes.

The main entry point to the unreachable tactic linter.

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