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.

Equations

• Lean.Substring.Raw.getRange { str := str, startPos := st, stopPos := en } = { start := st, stop := en }

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.

Equations

• stx.filterMap f = (stx.filterMapM fun (x : Lean.Syntax) => pure (f x)).run

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

• stx.filter f = stx.filterMap fun (s : Lean.Syntax) => if f s = true then some s else none

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

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• Mathlib.Linter.EmptyLine.SkippedFileSegments = ((Std.HashSet.emptyWithCapacity.insert `Tactic).insert `Util).insert `Meta

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.

Equations

• One or more equations did not get rendered due to their size.