Linters for Mathlib

In this file we define additional linters for mathlib.

Perhaps these should be moved to Batteries in the future.

def Std.Tactic.Lint.structureInType : Std.Tactic.Lint.Linter

Linter that checks whether a structure should be in Prop.

Equations

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

def Std.Tactic.Lint.deprecatedNoSince : Std.Tactic.Lint.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.

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.

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

def Mathlib.Linter.DupNamespaceLinter.getLinterDupNamespace (o : Lean.Options) : Bool

Gets the value of the linter.dupNamespace option.

Equations

• Mathlib.Linter.DupNamespaceLinter.getLinterDupNamespace o = Lean.Linter.getLinterValue Mathlib.Linter.linter.dupNamespace o

partial def Mathlib.Linter.DupNamespaceLinter.getIds : Lean.Syntax → Array Lean.Syntax

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.

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.