[Agda] dependency graph

[Nils Anders Danielsson]

On 07/01/2019 17.48, Martin Escardo wrote:
> Is there a way to get a dependency graph of all (global) defined names
> in a set of Agda files?

Yes, for instance by editing the Agda source code and adding such a
feature. The logic for the current --dependency-graph option is
implemented mainly in Agda.Interaction.Highlighting.Dot. I assume that
it would be fairly easy to construct a similar feature that worked on
the level of top-level definitions instead of top-level modules.

Do you want to look at the dependency graph, or do you want to query it?

-- 
/NAD