Documentation

Mathlib.Tactic.Linter.Lint

Linters for Mathlib #

In this file we define additional linters for mathlib.

Perhaps these should be moved to Batteries in the future.

Linter that checks whether a structure should be in Prop.

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

    Linter that check that all deprecated tags come with since dates.

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

      dupNamespace linter #

      The dupNamespace linter produces a warning when a declaration contains the same namespace at least twice consecutively.

      For instance, Nat.Nat.foo and One.two.two trigger a warning, while Nat.One.Nat does not.

      The dupNamespace linter is set on by default. Lean emits a warning on any declaration that contains the same namespace at least twice consecutively.

      For instance, Nat.Nat.foo and One.two.two trigger a warning, while Nat.One.Nat does not.

      Note. This linter will not detect duplication in namespaces of autogenerated declarations (other than the one whose declId is present in the source declaration).

      getIds stx extracts the declId nodes from the Syntax stx. If stx is an alias or an export, then it extracts an ident, instead of a declId.

      The dupNamespace linter is set on by default. Lean emits a warning on any declaration that contains the same namespace at least twice consecutively.

      For instance, Nat.Nat.foo and One.two.two trigger a warning, while Nat.One.Nat does not.

      Note. This linter will not detect duplication in namespaces of autogenerated declarations (other than the one whose declId is present in the source declaration).

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

        oneLineAlign linter #

        The oneLineAlign linter checks that #align statements span a single line, which is desirable as it allows them to be parsed by very simple parsers.

        The oneLineAlign linter is set on by default. Lean emits a warning on #align statements spanning more than one line.

        The oneLineAlign linter is set on by default. Lean emits a warning on #align statements spanning more than one line.

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

          The "missing end" linter #

          The "missing end" linter emits a warning on non-closed sections and namespaces. It allows the "outermost" noncomputable section to be left open (whether or not it is named).

          The "missing end" linter emits a warning on non-closed sections and namespaces. It allows the "outermost" noncomputable section to be left open (whether or not it is named).

          The "missing end" linter emits a warning on non-closed sections and namespaces. It allows the "outermost" noncomputable section to be left open (whether or not it is named).

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