mathlib documentation

core.init.meta.has_reflect

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

Instances
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
@[instance]
meta def nat.reflect  :
has_reflect ℕ

source
@[instance]
meta def unsigned.reflect  :
has_reflect unsigned

source
@[instance]
meta def name.reflect  :
has_reflect name

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

source
@[instance]
meta def punit.reflect  :
has_reflect punit