mathlib documentation

core.​init.​meta.​mk_has_reflect_instance

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