EmptyLine
📁 Source: Mathlib/Tactic/Linter/EmptyLine.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsgetRange, filter, filterMap, filterMapM, AllowEmptyLines, SkippedFileSegments, emptyLineLinter, emptyLine | 8 |
| Theorems | 0 |
| Total | 8 |
Lean.Substring.Raw
Definitions
| Name | Category | Theorems |
|---|---|---|
getRange 📖 | CompOp | — |
Lean.Syntax
Definitions
| Name | Category | Theorems |
|---|---|---|
filter 📖 | CompOp | — |
filterMap 📖 | CompOp | — |
filterMapM 📖 | CompOp | — |
Mathlib.Linter.EmptyLine
Definitions
| Name | Category | Theorems |
|---|---|---|
AllowEmptyLines 📖 | CompOp | — |
SkippedFileSegments 📖 | CompOp | — |
emptyLineLinter 📖 | CompOp | — |
Mathlib.Linter.linter.style
Definitions
| Name | Category | Theorems |
|---|---|---|
emptyLine 📖 | CompOp | — |
---