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

def Batteries.Linter.UnnecessarySeqFocus.getLinterUnnecessarySeqFocus (o : Lean.Linter.LinterOptions) : Bool

Gets the value of the linter.unnecessarySeqFocus option.

Equations

• Batteries.Linter.UnnecessarySeqFocus.getLinterUnnecessarySeqFocus o = Lean.Linter.getLinterValue Batteries.Linter.linter.unnecessarySeqFocus o

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.

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.

@[reducible, inline]

abbrev Batteries.Linter.UnnecessarySeqFocus.M (ω α : Type) : Type

The monad for collecting used tactic syntaxes.

Equations

• Batteries.Linter.UnnecessarySeqFocus.M ω = StateRefT' ω (Std.HashMap Lean.Syntax.Range Batteries.Linter.UnnecessarySeqFocus.Entry) (ST ω)

@[inline]

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

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

Equations

• Batteries.Linter.UnnecessarySeqFocus.isSeqFocus k = (k == `Lean.Parser.Tactic.«tactic_<;>_» || k == `Lean.Parser.Tactic.Conv.«conv_<;>_»)

@[specialize #[]]

partial def Batteries.Linter.UnnecessarySeqFocus.getTactics {ω : Type} (stx : Lean.Syntax) : M ω Unit

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

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

• One or more equations did not get rendered due to their size.
• Batteries.Linter.UnnecessarySeqFocus.getPath x✝¹ x✝ [] = some x✝¹

partial def Batteries.Linter.UnnecessarySeqFocus.markUsedTacticsList (env : Lean.Environment) {ω : Type} (trees : Lean.PersistentArray Lean.Elab.InfoTree) : M ω Unit

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

partial def Batteries.Linter.UnnecessarySeqFocus.markUsedTactics (env : Lean.Environment) {ω : Type} : Lean.Elab.InfoTree → M ω Unit

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

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.