Documentation

Mathlib.Tactic.Linter.EmptyLine

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.

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.

    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.

      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

        The SyntaxNodeKinds where the EmptyLine linter is not active

        Instances For
          source
          @[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.

          Instances For
            source
            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.

            Instances For