UnreachableTactic

📁 Source: Batteries/Linter/UnreachableTactic.lean

Statistics

Metric	Count
Definitions M, addIgnoreTacticKind, eraseUsedTactics, eraseUsedTacticsList, getLinterUnreachableTactic, getTactics, ignoreTacticKindsRef, isIgnoreTacticKind, unreachableTacticLinter, unreachableTactic	10
Theorems	0
Total	10

Batteries.Linter.UnreachableTactic

Definitions

Name	Category	Theorems
M 📖	CompOp	—
addIgnoreTacticKind 📖	CompOp	—
eraseUsedTactics 📖	CompOp	—
eraseUsedTacticsList 📖	CompOp	—
getLinterUnreachableTactic 📖	CompOp	—
getTactics 📖	CompOp	—
ignoreTacticKindsRef 📖	CompOp	—
isIgnoreTacticKind 📖	CompOp	—
unreachableTacticLinter 📖	CompOp	—

Batteries.Linter.linter

Definitions

Name	Category	Theorems
unreachableTactic 📖	CompOp	—

---

← Back to Index