mathlib3 documentation

core / init.meta.has_reflect

source
@[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 α.

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

Instances that [derive] depends on. All other basic instances are defined at the end of derive.lean.

source
@[protected, instance]
meta def name.reflect  :
has_reflect name
source
@[protected, instance]
meta def list.reflect {α : Type} [has_reflect α] [reflected Type α] :
has_reflect (list α)
source
@[protected, instance]
meta def punit.reflect  :
has_reflect punit