opaque Batteries.Linter.linter.unreachableTactic : Lean.Option Bool

Enables the 'unreachable tactic' linter. This will warn on any tactics that are never executed. For example, in example : True := by trivial <;> done, the tactic done is never executed because trivial produces no subgoals; you could put sorry or apply I_don't_exist or anything else there and no error would result.

A common source of such things is simp <;> tac in the case that simp improves and closes a subgoal that was previously being closed by tac.

def Batteries.Linter.UnreachableTactic.getLinterUnreachableTactic (o : Lean.Options) : Bool

Gets the value of the linter.unreachableTactic option.

Equations

• Batteries.Linter.UnreachableTactic.getLinterUnreachableTactic o = Lean.Linter.getLinterValue Batteries.Linter.linter.unreachableTactic o

@[reducible, inline]

abbrev Batteries.Linter.UnreachableTactic.M (α : Type) : Type

The monad for collecting used tactic syntaxes.

Equations

• Batteries.Linter.UnreachableTactic.M = StateRefT' IO.RealWorld (Std.HashMap String.Range Lean.Syntax) IO

opaque Batteries.Linter.UnreachableTactic.ignoreTacticKindsRef : IO.Ref Lean.NameHashSet

A list of blacklisted syntax kinds, which are expected to have subterms that contain unevaluated tactics.

def Batteries.Linter.UnreachableTactic.isIgnoreTacticKind (ignoreTacticKinds : Lean.NameHashSet) (k : Lean.SyntaxNodeKind) : Bool

Is this a syntax kind that contains intentionally unevaluated tactic subterms?

Equations

• Batteries.Linter.UnreachableTactic.isIgnoreTacticKind ignoreTacticKinds (pre.str "quot") = true
• Batteries.Linter.UnreachableTactic.isIgnoreTacticKind ignoreTacticKinds k = ignoreTacticKinds.contains k

def Batteries.Linter.UnreachableTactic.addIgnoreTacticKind (kind : Lean.SyntaxNodeKind) : IO Unit

Adds a new syntax kind whose children will be ignored by the unreachableTactic linter. This should be called from an initialize block.

Equations

• Batteries.Linter.UnreachableTactic.addIgnoreTacticKind kind = ST.Ref.modify Batteries.Linter.UnreachableTactic.ignoreTacticKindsRef fun (x : Lean.NameHashSet) => x.insert kind

@[specialize #[]]

partial def Batteries.Linter.UnreachableTactic.getTactics (ignoreTacticKinds : Lean.NameHashSet) (isTacKind : Lean.SyntaxNodeKind → Bool) (stx : Lean.Syntax) : Batteries.Linter.UnreachableTactic.M Unit

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

partial def Batteries.Linter.UnreachableTactic.eraseUsedTacticsList (trees : Lean.PersistentArray Lean.Elab.InfoTree) : Batteries.Linter.UnreachableTactic.M Unit

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

partial def Batteries.Linter.UnreachableTactic.eraseUsedTactics : Lean.Elab.InfoTree → Batteries.Linter.UnreachableTactic.M Unit

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

def Batteries.Linter.UnreachableTactic.unreachableTacticLinter : Lean.Linter

Enables the 'unreachable tactic' linter. This will warn on any tactics that are never executed. For example, in example : True := by trivial <;> done, the tactic done is never executed because trivial produces no subgoals; you could put sorry or apply I_don't_exist or anything else there and no error would result.

A common source of such things is simp <;> tac in the case that simp improves and closes a subgoal that was previously being closed by tac.

Equations

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