# 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.

source
def Batteries.Tactic.Lint.structureInType :
Linter

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

source
def Batteries.Tactic.Lint.deprecatedNoSince :
Linter

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.

source
opaque Mathlib.Linter.linter.dupNamespace :
Lean.Option Bool

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

source
def Mathlib.Linter.DupNamespaceLinter.dupNamespace :
Lean.Linter

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