HepLean 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.Options) :
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
    structure Batteries.Linter.UnnecessarySeqFocus.Entry :
    Type

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

    • stx : Lean.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
      source
      @[reducible, inline]
      abbrev Batteries.Linter.UnnecessarySeqFocus.M (ω : Type) (α : Type) :
      Type

      The monad for collecting used tactic syntaxes.

      Equations
      Instances For
        source
        @[inline]
        def Batteries.Linter.UnnecessarySeqFocus.isSeqFocus (k : Lean.SyntaxNodeKind) :
        Bool

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

        Equations
        Instances For
          source
          @[specialize #[]]
          partial def Batteries.Linter.UnnecessarySeqFocus.getTactics {ω : Type} (stx : Lean.Syntax) :
          Batteries.Linter.UnnecessarySeqFocus.M ω Unit

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

          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) {ω : Type} (trees : Lean.PersistentArray Lean.Elab.InfoTree) :
            Batteries.Linter.UnnecessarySeqFocus.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) {ω : Type} :
            Lean.Elab.InfoTree → Batteries.Linter.UnnecessarySeqFocus.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