ink

opaque Std.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

ink

def Std.Linter.UnnecessarySeqFocus.getLinterUnnecessarySeqFocus (o : Lean.Options) : Bool

Gets the value of the linter.unnecessarySeqFocus option.

Equations

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

ink

opaque Std.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.

ink

structure Std.Linter.UnnecessarySeqFocus.Entry : Type

• The <;> node itself.

  stx : Lean.Syntax
• • 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.
  used : Bool

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

ink

@[inline]

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

The monad for collecting used tactic syntaxes.

Equations

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

ink

@[inline]

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

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

Equations

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

ink

@[specialize #[]]

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

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

ink

def Std.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.
• Std.Linter.UnnecessarySeqFocus.getPath x x [] = some x

ink

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

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

ink

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

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

ink

def Std.Linter.UnnecessarySeqFocus.unnecessarySeqFocusLinter : Lean.Linter

The main entry point to the unused tactic linter.

Equations

• One or more equations did not get rendered due to their size.