command to list unused decls in files

Stream: general

[Johan Commelin]

I'm slowly recovering from some mild illness and my brain is still mashed potatoes...
There is a command to list all decls in a file that are not used by some given decl. I thought it was #show_unused. But my Lean disagrees.
What was it again? And can we please list a bunch of new MWE techniques in #mwe?

[Damiano Testa]

The command seems to exist:

import Batteries.Tactic.ShowUnused

theorem XX : True := .intro

theorem YY : True := XX

theorem ZZ : True := YY

#show_unused YY

[Damiano Testa]

It tells you that ZZ is not used in YY.

[Yaël Dillies]

Maybe it should be imported in Mathlib.Init?

[Ruben Van de Velde]

Is it imported anywhere in mathlib right now or did it fall victim to Kim's import minimizations?

[Johan Commelin]

Thanks!

[Damiano Testa]

It is not imported anywhere before Mathlib.lean, that now imports Batteries.

[Damiano Testa]

Yaël Dillies said:

Maybe it should be imported in Mathlib.Init?

I would be in favour of this. Besides, the imports of the command are Lean.Util.FoldConsts and Lean.Linter.UnusedVariables: the first I consider to be a quite basic file, the second "is" the UnusedVariables linter and should definitely be in Mathlib.Init!