Documentation

Lean.Linter.Extra.UnnecessarySeqFocus

source
opaque Lean.Linter.Extra.linter.extra.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
opaque Lean.Linter.Extra.UnnecessarySeqFocus.multigoalKindsRef :
IO.Ref NameSet

The set of tactic syntax kinds that act on multiple goals — meaning tac differs from focus tac. Used to suppress false positives where tac1 <;> tac2 cannot be replaced by (tac1; tac2) because that would expose tac2 to a different set of goals.

Other modules can extend this set in their own builtin_initialize block by calling addBuiltinMultigoalKinds.

source
def Lean.Linter.Extra.UnnecessarySeqFocus.addBuiltinMultigoalKind (k : SyntaxNodeKind) :
IO Unit

Register k as a multigoal tactic syntax kind.

Equations
Instances For
    source
    def Lean.Linter.Extra.UnnecessarySeqFocus.addBuiltinMultigoalKinds (ks : Array SyntaxNodeKind) :
    IO Unit

    Register ks as multigoal tactic syntax kinds.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Linter.Extra.UnnecessarySeqFocus.isMultigoalKind (k : SyntaxNodeKind) :
      BaseIO Bool

      Whether k is a multigoal tactic kind, per multigoalKindsRef.

      Equations
      Instances For
        source
        structure Lean.Linter.Extra.UnnecessarySeqFocus.Entry :
        Type

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

        • stx : 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 Lean.Linter.Extra.UnnecessarySeqFocus.M (ω α : Type) :
          Type

          The monad for collecting used tactic syntaxes.

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

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

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

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

              source
              def Lean.Linter.Extra.UnnecessarySeqFocus.getPath :
              Elab.Info → PersistentArray Elab.InfoTree → List ((n : Nat) × Fin n) → Option 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 Lean.Linter.Extra.UnnecessarySeqFocus.markUsedTacticsList (multigoals : NameSet) {ω : Type} (trees : PersistentArray Elab.InfoTree) :
                M ω Unit

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

                source
                partial def Lean.Linter.Extra.UnnecessarySeqFocus.markUsedTactics (multigoals : NameSet) {ω : Type} :
                Elab.InfoTree → M ω Unit

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

                source
                def Lean.Linter.Extra.UnnecessarySeqFocus.unnecessarySeqFocusLinter :
                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