Check which imported definitions are used

Stream: Is there code for X?

[Thomas Murrills]

Is there a way to check which imported definitions are actually used in a file? For example, if file1 defines f, g, and h, and in file2 I have import file1 and only use f (without redefining it), is there some command like #printDeps file1 which would print the name f?

[Eric Wieser]

You could certainly write such a command yourself, though I suspect it doesn't already exist. Leancrawler likely can do this from Python too.

[Floris van Doorn]

The command #list_unused_decls will do this, but you have to tag some declarations with @[main_theorem].

[Floris van Doorn]

(Well, it will print all the unused declarations, so it's almost what you asked)