# 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:

• @[std_linter] applies to a declaration of type Linter and adds it to the default linter set.

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

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.
• test defines a test to perform on every declaration. It should never fail. Returning none signifies a passing test. Returning some msg reports a failing test with error msg.

test :
• noErrorsFound is the message printed when all tests are negative

noErrorsFound : Lean.MessageData
• errorsFound is printed when at least one test is positive

errorsFound : Lean.MessageData
• If isFast is false, this test will be omitted from #lint-.

isFast : Bool

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
def Std.Tactic.Lint.getLinter (name : Lean.Name) (declName : Lean.Name) :

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 : } [inst : ] [inst : ] (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.