Documentation

Batteries.Linter.UnnecessarySeqFocus

source
opaque Batteries.Linter.linter.unnecessarySeqFocus :
Lean.Option Bool

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
source
def Batteries.Linter.UnnecessarySeqFocus.getLinterUnnecessarySeqFocus (o : Lean.Linter.LinterOptions) :
Bool

Gets the value of the linter.unnecessarySeqFocus option.

Equations
Instances For
    source
    opaque Batteries.Linter.UnnecessarySeqFocus.multigoalAttr :
    Lean.TagAttributeExtra

    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.

    source
    @[reducible, inline]
    abbrev Batteries.Linter.UnnecessarySeqFocus.M (α : Type) :
    Type

    The monad for collecting used tactic syntaxes.

    • some stx means that this <;> syntax has only been used unnecessarily.
    • none means that this <;> syntax was necessary at least once, so we won't warn about it.
    Equations
    Instances For
      source
      def Batteries.Linter.UnnecessarySeqFocus.getPath :
      Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List ((n : Nat) × Fin n) → Option Lean.Elab.Info

      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
        source
        partial def Batteries.Linter.UnnecessarySeqFocus.markUsedTacticsList (env : Lean.Environment) (trees : Lean.PersistentArray Lean.Elab.InfoTree) :
        M Unit

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

        source
        partial def Batteries.Linter.UnnecessarySeqFocus.markUsedTactics (env : Lean.Environment) :
        Lean.Elab.InfoTree → M Unit

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

        source
        def Batteries.Linter.UnnecessarySeqFocus.unnecessarySeqFocusLinter :
        Lean.Linter

        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