## Stream: general

### Topic: detecting hypotheses introduced by the equation compiler?

#### 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?

#### Mario Carneiro (Mar 12 2019 at 10:46):

look for aux_decl binders in the local constants

#### Scott Morrison (Mar 12 2019 at 10:48):

ah: expr.is_aux_decl

Last updated: May 11 2021 at 22:14 UTC