detecting hypotheses introduced by the equation compiler?

Stream: general

[Scott Morrison]

(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]

look for aux_decl binders in the local constants

[Scott Morrison]

ah: expr.is_aux_decl