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.

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 component of a declaration name is repeated several times. The repetition does not have to be consecutive. Examples: Nat.Nat.foo, One.two.two, Nat.One.Nat, Nat.Prime.Nat.Prime.foo, Nat.Prime.Nat.bar

      The linter also warns about auto-generated declarations (such as, those generated by to_additive).

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

      The dupNamespace linter produces a warning when a component of a declaration name is repeated several times. The repetition does not have to be consecutive. Examples: Nat.Nat.foo, One.two.two, Nat.One.Nat, Nat.Prime.Nat.Prime.foo, Nat.Prime.Nat.bar

      The linter also warns about auto-generated declarations (such as, those generated by to_additive).