Dependency Graph Generation

Stream: lean4

[madab]

Hi, I am trying to automatically generate the dependency graph for a given theorem in Lean4. Are there tools that already do this? And if I want to do this myself, can someone point me in the right direction?

[Kim Morrison]

Check out https://github.com/leanprover-community/import-graph for file level dependency graphs.

For declaration level dependencies, start with docs#Lean.ConstantInfo.getUsedConstantsAsSet