mathlib documentation

core / init.meta.has_reflect

@[reducible]
meta def has_reflect (α : Sort u) :
Sort (max u 1)

has_reflect α lets you produce an expr from an instance of α. That is, it is a function from α to expr such that the expr has type α.

meta structure reflected_value (α : Type u) :
Type u
meta def reflected_value.expr {α : Type u} (v : reflected_value α) :
meta def reflected_value.subst {α : Type u} {β : Type v} (f : α → β) [rf : reflected (α → β) f] (a : reflected_value α) :
@[protected, instance]
meta def nat.reflect  :
@[protected, instance]
@[protected, instance]
@[protected, instance]
meta def list.reflect {α : Type} [has_reflect α] [reflected Type α] :
@[protected, instance]