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.

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

opaque Mathlib.Linter.linter.missingEnd : Lean.Option Bool

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

def Mathlib.Linter.MissingEnd.getLinterHash (o : Lean.Options) : Bool

Gets the value of the linter.missingEnd option.

Equations

• Mathlib.Linter.MissingEnd.getLinterHash o = Lean.Linter.getLinterValue Mathlib.Linter.linter.missingEnd o

def Mathlib.Linter.MissingEnd.missingEndLinter : Lean.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).

Equations

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

The cdot linter

The cdot linter is a syntax-linter that flags uses of the "cdot" · that are achieved by typing a character different from ·. For instance, a "plain" dot . is allowed syntax, but is flagged by the linter.

opaque Mathlib.Linter.linter.cdot : Lean.Option Bool

The cdot linter flags uses of the "cdot" · that are achieved by typing a character different from ·. For instance, a "plain" dot . is allowed syntax, but is flagged by the linter.

def Mathlib.Linter.isCDot? : Lean.Syntax → Bool

isCDot? stx checks whether stx is a Syntax node corresponding to a cdot typed with the character ·.

Equations

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

partial def Mathlib.Linter.findCDot : Lean.Syntax → Array Lean.Syntax

findCDot stx extracts from stx the syntax nodes of kind Lean.Parser.Term.cdot or cdotTk.

def Mathlib.Linter.unwanted_cdot (stx : Lean.Syntax) : Array Lean.Syntax

unwanted_cdot stx returns an array of syntax atoms within stx corresponding to cdots that are not written with the character ·. This is precisely what the cdot linter flags.

Equations

• Mathlib.Linter.unwanted_cdot stx = Array.filter (fun (x : Lean.Syntax) => !Mathlib.Linter.isCDot? x) (Mathlib.Linter.findCDot stx) 0

def Mathlib.Linter.CDotLinter.getLinterHash (o : Lean.Options) : Bool

Gets the value of the linter.generic option.

Equations

• Mathlib.Linter.CDotLinter.getLinterHash o = Lean.Linter.getLinterValue Mathlib.Linter.linter.cdot o

def Mathlib.Linter.CDotLinter.cdotLinter : Lean.Linter

The cdot linter flags uses of the "cdot" · that are achieved by typing a character different from ·. For instance, a "plain" dot . is allowed syntax, but is flagged by the linter.

Equations

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

opaque Mathlib.Linter.linter.longLine : Lean.Option Bool

The "longLine" linter emits a warning on lines longer than 100 characters. We allow lines containing URLs to be longer, though.

def Mathlib.Linter.LongLine.getLinterHash (o : Lean.Options) : Bool

Gets the value of the linter.longLine option.

Equations

• Mathlib.Linter.LongLine.getLinterHash o = Lean.Linter.getLinterValue Mathlib.Linter.linter.longLine o

def Mathlib.Linter.LongLine.longLineLinter : Lean.Linter

The "longLine" linter emits a warning on lines longer than 100 characters. We allow lines containing URLs to be longer, though.

Equations

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