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

Defines the user attribute nolint for skipping #lint

meta def should_be_linted (linter decl : name) :

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

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.

meta def get_linters (l : list name) :

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

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.