Which function causes dependency on an axiom?

Stream: general

[Yury G. Kudryashov]

How can I find which part of a definition/proof makes the result depend on an axiom?

[Rob Lewis]

Unfortunately there's no metaprogramming API for #print axioms. If you need this as a one-time thing, it's probably easiest to start defining subterms manually. The "proper" way would be to write a find_axioms tactic. It should produce an rb_lmap name name that you can then use on the expression tree. There are subtleties in identifying which constants are "really" axioms -- you probably want to ignore things like recursors, inductive type constructors, etc. It would be easier if you know which constants you're looking for at the beginning.