The "emptyLine" linter

The "emptyLine" linter emits a warning on empty lines inside a command, but outside of a doc-string/module-doc.

def Lean.Substring.Raw.getRange : Substring.Raw → Syntax.Range

Retrieve the String.Range of a Substring.

Syntax filters

partial def Lean.Syntax.filterMapM {m : Type → Type} [Monad m] {α : Type} (stx : Syntax) (f : Syntax → m (Option α)) : m (Array α)

filterMapM stx f takes as input a Syntax stx and a monadic function f : Syntax → m α. It produces the array of the some values that f takes while traversing stx.

See filterMap for a non-monadic version.

def Lean.Syntax.filterMap {α : Type} (stx : Syntax) (f : Syntax → Option α) : Array α

filterMap stx f takes as input a Syntax stx and a function f : Syntax → α. It produces the array of the some values that f takes while traversing stx.

See filterMapM for a non-monadic version.

def Lean.Syntax.filter (stx : Syntax) (f : Syntax → Bool) : Array Syntax

filter stx f takes as input a Syntax stx and a function f : Syntax → Bool. It produces the array of the syntax nodes in stx where f is true.

See also the similar filterMap and filterMapM.

opaque Mathlib.Linter.linter.style.emptyLine : Lean.Option Bool

The "emptyLine" linter emits a warning on empty lines inside a command, but outside of a doc-string/module-doc.

The linter is only active when there are no other warnings, so as to not add noise when developing incomplete proofs.

@[reducible, inline]

abbrev Mathlib.Linter.EmptyLine.AllowEmptyLines : Std.HashSet Lean.SyntaxNodeKind

The SyntaxNodeKinds where the EmptyLine linter is not active

@[reducible, inline]

abbrev Mathlib.Linter.EmptyLine.SkippedFileSegments : Std.HashSet Lean.Name

If a file contains one of these names as segments, we disable the emptyLine linter.

def Mathlib.Linter.EmptyLine.emptyLineLinter : Lean.Linter

The "emptyLine" linter emits a warning on empty lines inside a command, but outside of a doc-string/module-doc.

The linter is only active when there are no other warnings, so as to not add noise when developing incomplete proofs.