mathlib documentation

core / init.meta.has_reflect

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 α) :

meta def nat.reflect  :



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