list_unused_decls #
#list_unused_decls
is a command used for theory development.
When writing a new theory one often tries
multiple variations of the same definitions: foo
, foo'
, foo₂
,
foo₃
, etc. Once the main definition or theorem has been written,
it's time to clean up and the file can contain a lot of dead code.
Mark the main declarations with @[main_declaration]
and
#list_unused_decls
will show the declarations in the file
that are not needed to define the main declarations.
Some of the so-called "unused" declarations may turn out to be useful
after all. The oversight can be corrected by marking those as
@[main_declaration]
. #list_unused_decls
will revise the list of
unused declarations. By default, the list of unused declarations will
not include any dependency of the main declarations.
The @[main_declaration]
attribute should be removed before submitting
code to mathlib as it is merely a tool for cleaning up a module.