Documentation

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

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 information we record for each <;> node appearing in the syntax.

  • The <;> node itself.

  • used : Bool
    • 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.
@[reducible, inline]

The monad for collecting used tactic syntaxes.

Equations
@[inline]

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

Equations
@[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

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.

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
Equations
  • One or more equations did not get rendered due to their size.