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

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.

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

Register k as a multigoal tactic syntax kind.

def Lean.Linter.Extra.UnnecessarySeqFocus.addBuiltinMultigoalKinds (ks : Array SyntaxNodeKind) : IO Unit

Register ks as multigoal tactic syntax kinds.

def Lean.Linter.Extra.UnnecessarySeqFocus.isMultigoalKind (k : SyntaxNodeKind) : BaseIO Bool

Whether k is a multigoal tactic kind, per multigoalKindsRef.

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.

@[reducible, inline]

abbrev Lean.Linter.Extra.UnnecessarySeqFocus.M (ω α : Type) : Type

The monad for collecting used tactic syntaxes.

@[inline]

def Lean.Linter.Extra.UnnecessarySeqFocus.isSeqFocus (k : SyntaxNodeKind) : Bool

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

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

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.

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.

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.

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