Function dependency_graph 

pub fn dependency_graph(
    definitions: &[Definition],
    premises: &[ProofExpr],
    goal: &ProofExpr,
) -> DependencyGraph

Build the DependencyGraph for a set of definitions plus a theorem (premises + goal), recording which definitions each definiens uses and which the theorem uses. Pure, allocation-light, O(total expression size).