Documentation
Lean
.
Linter
.
Extra
Search
return to top
source
Imports
Lean.Linter.Extra.DupNamespace
Lean.Linter.Extra.UnnecessarySeqFocus
Lean.Linter.Extra.UnreachableTactic
Lean.Linter.Extra.UnusedDecidableInType
Imported by
← Mathematical handbook