Zulip Chat Archive

Stream: general

Topic: detecting hypotheses introduced by the equation compiler?


view this post on Zulip Scott Morrison (Mar 12 2019 at 10:42):

(For the purposes of some automation) I'd like to treat hypotheses that were introduced by the equation compiler (e.g. the inductive hypothesis) differently from the others. Is there a way of inspecting the local_context and determining which ones these are?

view this post on Zulip Mario Carneiro (Mar 12 2019 at 10:46):

look for aux_decl binders in the local constants

view this post on Zulip Scott Morrison (Mar 12 2019 at 10:48):

ah: expr.is_aux_decl


Last updated: May 11 2021 at 22:14 UTC