Basic
📁 Source: Batteries/Tactic/Lint/Basic.lean
Statistics
| Metric | Count |
|---|---|
DefinitionserrorsFound, isFast, noErrorsFound, test, NamedLinter, declName, name, toLinter, batteriesLinterExt, env_linter, getLinter, isAutoDecl, nolint, nolintAttr, shouldBeLinted | 15 |
| Theorems | 0 |
| Total | 15 |
Batteries.Tactic.Lint
Definitions
| Name | Category | Theorems |
|---|---|---|
NamedLinter 📖 | CompData | — |
batteriesLinterExt 📖 | CompOp | — |
env_linter 📖 | CompOp | — |
getLinter 📖 | CompOp | — |
isAutoDecl 📖 | CompOp | — |
nolint 📖 | CompOp | — |
nolintAttr 📖 | CompOp | — |
shouldBeLinted 📖 | CompOp | — |
Batteries.Tactic.Lint.Linter
Definitions
| Name | Category | Theorems |
|---|---|---|
errorsFound 📖 | CompOp | — |
isFast 📖 | CompOp | — |
noErrorsFound 📖 | CompOp | — |
test 📖 | CompOp | — |
Batteries.Tactic.Lint.NamedLinter
Definitions
| Name | Category | Theorems |
|---|---|---|
declName 📖 | CompOp | — |
name 📖 | CompOp | — |
toLinter 📖 | CompOp | — |
---