Function axiom_dependencies_given 

pub fn axiom_dependencies_given(
    ctx: &Context,
    term: &Term,
    known: &dyn Fn(&str) -> Option<Vec<String>>,
) -> AxiomUsage

The axiom closure of term, as axiom_dependencies, where known answers the axioms of a constant whose closure was already taken: the walk takes that answer at the constant instead of walking below it. Reachability is transitive, so the answer is what the walk would have found there, and a constant whose closure was taken had every name below it resolved. An importer that audits each declaration in order passes the sets it recorded, so a declaration’s walk covers its own terms and what is not yet audited rather than the whole closure again.