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):
aux_decl binders in the local constants
Scott Morrison (Mar 12 2019 at 10:48):
Last updated: May 11 2021 at 22:14 UTC