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 section
s and namespace
s.
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 section
s and namespace
s.
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 section
s and namespace
s.
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.