pub fn axiom_dependencies(ctx: &Context, term: &Term) -> AxiomUsageExpand description
Every AXIOM a term actually depends on — Lean’s #print axioms, as a function.
The closure is TRANSITIVE through definitions, following both a definition’s BODY and its TYPE
(a type can cite an axiom the body never mentions). A one-hop scan of a proof term sees only the
lemma it names, which is precisely how a sorry three lemmas upstream stays invisible.
A name that resolves to nothing is reported too, in unresolved: a proof naming a constant the
trusted base does not have IS trusted-base drift, and it must be visible as that rather than as
a name-resolution symptom.
Lives in prelude rather than in certificate on purpose. certificate is behind the serde
feature; the audit trail is not optional, and the REPL’s Print Axioms, the kernel’s own
diagnostics and logicaffeine_proof’s verdicts all need it in the default build.