Documentation

Std.Tactic.Lint.Basic

Basic linter types and attributes #

This file defines the basic types and attributes used by the linting framework. A linter essentially consists of a function (declaration : Name) → MetaM (Option MessageData), this function together with some metadata is stored in the Linter structure. We define two attributes:

Returns true if decl is an automatically generated declaration.

Also returns true if decl is an internal name or created during macro expansion.

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

A linting test for the #lint command.

Instances For
    • The name of the named linter. This is just the declaration name without the namespace.

      name : Lean.Name
    • The linter declaration name

      declName : Lean.Name

    A NamedLinter is a linter associated to a particular declaration.

    Instances For

      Gets a linter by declaration name.

      Equations

      Defines the std_linter extension for adding a linter to the default set.

      Defines the @[std_linter] attribute for adding a linter to the default set. The form @[std_linter disabled] will not add the linter to the default set, but it will be shown by #list_linters and can be selected by the #lint command.

      Linters are named using their declaration names, without the namespace. These must be distinct.

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

      @[nolint linterName] omits the tagged declaration from being checked by the linter with name linterName.

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

      Defines the user attribute nolint for skipping #lint

      def Std.Tactic.Lint.shouldBeLinted {m : TypeType} [inst : Monad m] [inst : Lean.MonadEnv m] (linter : Lean.Name) (decl : Lean.Name) :

      Returns true if decl should be checked using linter, i.e., if there is no nolint attribute.

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