Zulip Chat Archive

Stream: general

Topic: Which function causes dependency on an axiom?

view this post on Zulip 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?

view this post on Zulip 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