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

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

The monad for collecting used tactic syntaxes.

Equations

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

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

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

Instances For

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

source
partial 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.

source
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.

source
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.

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