The "emptyLine" linter #

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

source

def Lean.Substring.Raw.getRange :

Substring.Raw → Syntax.Range

Retrieve the String.Range of a Substring.

Equations

Instances For

`Syntax` filters #

source

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.

source

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.

Equations

Instances For

source

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.

Equations

Instances For

source

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.

source

@[reducible, inline]

abbrev Mathlib.Linter.EmptyLine.AllowEmptyLines :

Std.HashSet Lean.SyntaxNodeKind