Documentation
Batteries
.
Linter
.
UnnecessarySeqFocus
Search
return to top
source
Imports
Init
Batteries.Lean.AttributeExtra
Lean.Elab.Command
Lean.Linter.Basic
Imported by