Yury G. Kudryashov (Dec 05 2019 at 07:08):
How can I find which part of a definition/proof makes the result depend on an axiom?
Rob Lewis (Dec 05 2019 at 10:36):
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.
Last updated: May 08 2021 at 19:11 UTC