Documentation

Mathlib.Tactic.Linter.Lint

Linters for Mathlib #

In this file we define additional linters for mathlib, which concern the behaviour of the linted code, and not issues of code style or formatting.

Perhaps these should be moved to Batteries in the future.

Linter that checks whether a structure should be in Prop.

Equations
    Instances For

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

      Equations
        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).

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