Documentation

Mathlib.Tactic.Linter.Lint

Linters for Mathlib #

In this file we define additional linters for mathlib.

Perhaps these should be moved to Batteries 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
    source
    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.
    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
      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

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

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

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

          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.

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

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

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

                The "longLine linter" #

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

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