Frontend
📁 Source: Batteries/Tactic/Lint/Frontend.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsLintVerbosity, formatLinterResults, getAllDecls, getChecks, getDeclsInCurrModule, getDeclsInPackage, groupedByFilename, inProject, instDecidableEqLintVerbosity, instInhabitedLintVerbosity, default, instReprLintVerbosity, repr, lintCore, printWarning, printWarnings, sortResults, traceLint, traceLintCore, «command#lint+-*Only___», «command#list_linters» | 21 |
| Theorems | 0 |
| Total | 21 |
Batteries.Tactic.Lint
Definitions
| Name | Category | Theorems |
|---|---|---|
LintVerbosity 📖 | CompData | — |
formatLinterResults 📖 | CompOp | — |
getAllDecls 📖 | CompOp | — |
getChecks 📖 | CompOp | — |
getDeclsInCurrModule 📖 | CompOp | — |
getDeclsInPackage 📖 | CompOp | — |
groupedByFilename 📖 | CompOp | — |
inProject 📖 | CompOp | — |
instDecidableEqLintVerbosity 📖 | CompOp | — |
instInhabitedLintVerbosity 📖 | CompOp | — |
instReprLintVerbosity 📖 | CompOp | — |
lintCore 📖 | CompOp | — |
printWarning 📖 | CompOp | — |
printWarnings 📖 | CompOp | — |
sortResults 📖 | CompOp | — |
traceLint 📖 | CompOp | — |
traceLintCore 📖 | CompOp | — |
«command#lint+-*Only___» 📖 | CompOp | — |
«command#list_linters» 📖 | CompOp | — |
Batteries.Tactic.Lint.instInhabitedLintVerbosity
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Batteries.Tactic.Lint.instReprLintVerbosity
Definitions
| Name | Category | Theorems |
|---|---|---|
repr 📖 | CompOp | — |
---