Documentation

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

    A linting test for the #lint command.

    Instances For

      A NamedLinter is a linter associated to a particular declaration.

      Instances For

        Gets a linter by declaration name.

        Equations
        Instances For

          Defines the @[env_linter] attribute for adding a linter to the default set. The form @[env_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.
          Instances For

            @[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.
            Instances For

              Defines the user attribute nolint for skipping #lint

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

              Equations
              Instances For