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.
Instances For
    @[reducible, inline]

    The monad for collecting used tactic syntaxes.

    Equations
    Instances For
      @[inline]

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

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

          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.
          Instances For