mathlib3 documentation

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 → tactic (option string), this function together with some metadata is stored in the linter structure. We define two attributes:

source
meta def nolint_attr  :
user_attribute (name_map (list name)) (list name)

Defines the user attribute nolint for skipping #lint

source
def tactic_doc.attribute.nolint  :
tactic_doc_entry

Defines the user attribute nolint for skipping #lint

source
meta def should_be_linted (linter decl : name) :
tactic bool

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

source
meta structure linter  :
Type

A linting test for the #lint command.

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.

no_errors_found is the message printed when all tests are negative, and errors_found is printed when at least one test is positive.

If is_fast is false, this test will be omitted from #lint-.

If auto_decls is true, this test will also be executed on automatically generated declarations.

source
meta def get_linters (l : list name) :
tactic (list (name × linter))

Takes a list of names that resolve to declarations of type linter, and produces a list of linters.

source
meta def linter_attr  :
(user_attribute unit)

Defines the user attribute linter for adding a linter to the default set. Linters should be defined in the linter namespace. A linter linter.my_new_linter is referred to as my_new_linter (without the linter namespace) when used in #lint.

source
def tactic_doc.attribute.linter  :
tactic_doc_entry

Defines the user attribute linter for adding a linter to the default set. Linters should be defined in the linter namespace. A linter linter.my_new_linter is referred to as my_new_linter (without the linter namespace) when used in #lint.