Documentation Verification Report

UnnecessarySeqFocus

📁 Source: Batteries/Linter/UnnecessarySeqFocus.lean

Statistics

Metric	Count
Definitions `Entry`, `stx`, `used`, `M`, `getLinterUnnecessarySeqFocus`, `getPath`, `getTactics`, `isSeqFocus`, `markUsedTactics`, `markUsedTacticsList`, `multigoalAttr`, `unnecessarySeqFocusLinter`, `unnecessarySeqFocus`	13
Theorems	0
Total	13

Batteries.Linter.UnnecessarySeqFocus

Definitions

Name	Category	Theorems
`Entry` 📖	CompData	—
`M` 📖	CompOp	—
`getLinterUnnecessarySeqFocus` 📖	CompOp	—
`getPath` 📖	CompOp	—
`getTactics` 📖	CompOp	—
`isSeqFocus` 📖	CompOp	—
`markUsedTactics` 📖	CompOp	—
`markUsedTacticsList` 📖	CompOp	—
`multigoalAttr` 📖	CompOp	—
`unnecessarySeqFocusLinter` 📖	CompOp	—

Batteries.Linter.UnnecessarySeqFocus.Entry

Definitions

Name	Category	Theorems
`stx` 📖	CompOp	—
`used` 📖	CompOp	—

Batteries.Linter.linter

Definitions

Name	Category	Theorems
`unnecessarySeqFocus` 📖	CompOp	—

---

← Back to Index