4. Dependency Graph🔗

Interactive dependency view for exposed declarations.

An edge points from a dependency to the declaration that depends on it, following every dependency (both type and proof/body) of each declaration. Edges implied by a longer path through other edges are pruned (e.g. if A uses B and B uses C, the direct A → C edge is dropped when A also uses C only because B does), so only the most direct dependency relationships are drawn.