Axioms in axioms' types

Stream: lean4

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

When an axiom appears only in other axioms' types, it will not be printed by #print axioms. (This is a result of how docs#Lean.CollectAxioms.collect is implemented.) Is this correct?

axiom B : Type
axiom v : B
axiom c : B → Nat
noncomputable def a := c v

-- 'a' depends on axioms: [c, v]
#print axioms a

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Oh I take this back, it was fixed in lean#8842!