# mathlibdocumentation

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 α.