# Documentation

Std.Linter.UnnecessarySeqFocus

Enables the 'unnecessary <;>' linter. This will warn whenever the <;> tactic combinator is used when ; would work.

example : True := by apply id <;> trivial


The <;> is unnecessary here because apply id only makes one subgoal. Prefer apply id; trivial instead.

In some cases, the <;> is syntactically necessary because a single tactic is expected:

example : True := by
cases () with apply id <;> apply id
| unit => trivial


In this case, you should use parentheses, as in (apply id; apply id):

example : True := by
cases () with (apply id; apply id)
| unit => trivial


Gets the value of the linter.unnecessarySeqFocus option.

Equations

The multigoal attribute keeps track of tactics that operate on multiple goals, meaning that tac acts differently from focus tac. This is used by the 'unnecessary <;>' linter to prevent false positives where tac <;> tac' cannot be replaced by (tac; tac') because the latter would expose tac to a different set of goals.

• The <;> node itself.

• true: this <;> has been used unnecessarily at least once
• false: it has never been executed
• If it has been used properly at least once, the entry is removed from the table.
used : Bool

The information we record for each <;> node appearing in the syntax.

Instances For
@[inline]

The monad for collecting used tactic syntaxes.

Equations
@[inline]

True if this is a <;> node in either tactic or conv classes.

Equations
• = (k == Lean.Parser.Tactic.tactic_<>_ || k == Lean.Parser.Tactic.Conv.conv_<>_)
@[specialize #[]]

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

Traverse the info tree down a given path. Each (n, i) means that the array must have length n and we will descend into the i'th child.

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

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 unused tactic linter.

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