core / init.meta.mk_has_reflect_instance
source
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 α.
has_reflect α
reflected