mathlib documentation

core.init.meta.has_reflect

meta structure reflected_value  :
Type uType u

meta def reflected_value.expr {α : Type u} :

meta def reflected_value.subst {α : Type u} {β : Type v} (f : α → β) [rf : reflected f] :

@[instance]
meta def nat.reflect  :

@[instance]

@[instance]

@[instance]
meta def list.reflect {α : Type} [has_reflect α] [reflected α] :

@[instance]