Documentation

Mathlib.Tactic.Lint

Linters for Mathlib #

In this file we define additional linters for mathlib.

Perhaps these should be moved to Std in the future.

source
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.
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.getLinterDupNamespace (o : Lean.Options) :
    Bool

    Gets the value of the linter.dupNamespace option.

    Equations
    Instances For
      source
      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.

      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