tactic.lint.misc

# Various linters #

This file defines several small linters:

• ge_or_gt checks that > and ≥ do not occur in the statement of theorems.
• dup_namespace checks that no declaration has a duplicated namespace such as list.list.monad.
• unused_arguments checks that definitions and theorems do not have unused arguments.
• doc_blame checks that every definition has a documentation string.
• doc_blame_thm checks that every theorem has a documentation string (not enabled by default).
• def_lemma checks that a declaration is a lemma iff its type is a proposition.
• check_type checks that the statement of a declaration is well-typed.

## Linter against use of >/≥#

meta def linter.ge_or_gt  :

A linter for checking whether illegal constants (≥, >) appear in a declaration's type.

## Linter for duplicate namespaces #

A linter for checking whether a declaration has a namespace twice consecutively in its name.

## Linter for unused arguments #

Check which arguments of a declaration are not used. Prints a list of natural numbers corresponding to which arguments are not used (e.g. this outputs [1, 4] if the first and fourth arguments are unused). Checks both the type and the value of d for whether the argument is used (in rare cases an argument is used in the type but not in the value). We return [] if the declaration was automatically generated. We print arguments that are larger than the arity of the type of the declaration (without unfolding definitions).

A linter object for checking for unused arguments. This is in the default linter set.

## Linter for documentation strings #

meta def linter.doc_blame  :

A linter for checking definition doc strings

A linter for checking theorem doc strings. This is not in the default linter set.

## Linter for correct usage of lemma/def#

meta def linter.def_lemma  :

A linter for checking whether the correct declaration constructor (definition or theorem) has been used.

meta def check_type (d : declaration) :

Checks whether the statement of a declaration is well-typed.

meta def linter.check_type  :

A linter for missing checking whether statements of declarations are well-typed.