Solves a goal of the form has_reflect α
where α is an inductive type.
Needs to synthesize a reflected
instance for each inductive parameter type of α
and for each constructor parameter of α.
core.init.meta.mk_has_reflect_instance
Solves a goal of the form has_reflect α
where α is an inductive type.
Needs to synthesize a reflected
instance for each inductive parameter type of α
and for each constructor parameter of α.