opaque Std.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 Std.Linter.UnreachableTactic.getLinterUnreachableTactic (o : Lean.Options) : Bool

Gets the value of the linter.unreachableTactic option.

Equations

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

@[inline, reducible]

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

The monad for collecting used tactic syntaxes.

Equations

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

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

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

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

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

Equations

• Std.Linter.UnreachableTactic.isIgnoreTacticKind ignoreTacticKinds k = match k with | Lean.Name.str pre "quot" => true | x => Lean.NameHashSet.contains ignoreTacticKinds k

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

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

@[specialize #[]]

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

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

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

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

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

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

def Std.Linter.UnreachableTactic.unreachableTacticLinter : Lean.Linter

The main entry point to the unreachable tactic linter.

Equations

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