pub fn axiom_dependencies_of(ctx: &Context, name: &str) -> Option<AxiomUsage>Expand description
The axiom closure of a NAMED constant in a context — what Print Axioms <name>. reports.
A definition reports what its statement and body rest on; an axiom reports itself alone,
as Lean’s #print axioms does. None when the name is not registered.