A tool for finding duplicate declarations #
It is easy to accidentally create multiple instances of the same theorem or instance. This file defines a tool to automatically detect such cases. The order of hypotheses, and their binder info and binder names are ignored. Universe parameters are also ignored.
For theorems, it is completely redundant to have multiple of the same type. For instances, we typically also don't want to have multiple of the same type.
To use it, simply run the following command in a file that does not use the module system:
open Lean Mathlib.Tactic.DuplicateDecls
run_meta do logInfo m!"{← lintDuplicateDeclarations .theorems}"
run_meta do logInfo m!"{← lintDuplicateDeclarations .instances}"
run_meta do logInfo m!"{← lintDuplicateDeclarations .defs}"
How does it work #
The function sortBinders reorders the forall binders of a declaration type into a canonical form,
which lets us detect duplication even when the arguments are in a different order.
We also erase the binder kinds (e.g. implicit/explicit) in the type,
and we erase all universe levels, both of which help to find more duplicates.
To avoid flagging aliases as duplicate (which are most likely intentionally duplicated),
we filter out declarations that are defined as another declaration (see isAlias).
The results are sorted by module name.
An inductive type for the kind of duplicate declarations to search for.
- theorems : Target
Search for duplicate theorems.
- instances : Target
Search for duplicate instances that aren't theorems.
- defs : Target
Search for duplicate definitions that aren't instances or theorems, Also indexes on the value, not just the type.
Instances For
The duplicate declarations linter. It tells you which duplicate declarations there are in the current environment.
Equations
- One or more equations did not get rendered due to their size.