mathlib3 documentation

core / init.meta.pexpr

source
@[reducible]
meta def pexpr  :
Type

Quoted expressions. They can be converted into expressions by using a tactic.

source
@[protected]
meta constant pexpr.of_expr  :
expr → pexpr
source
meta constant pexpr.is_placeholder  :
pexpr → bool
source
meta constant pexpr.mk_placeholder  :
pexpr
source
meta constant pexpr.mk_field_macro  :
pexpr → name → pexpr
source
meta constant pexpr.mk_explicit  :
pexpr → pexpr
source
meta constant pexpr.is_choice_macro  :
pexpr → bool

Choice macros are used to implement overloading.

source
meta structure structure_instance_info  :
Type

Information about unelaborated structure instance expressions.

source
meta constant pexpr.mk_structure_instance  :
structure_instance_info → pexpr

Create a structure instance expression.

source
meta constant pexpr.get_structure_instance_info  :
pexpr → option structure_instance_info
source
@[class]
meta structure has_to_pexpr (α : Sort u) :
Sort (max 1 u)
Instances of this typeclass
source
meta def to_pexpr {α : Sort u} [has_to_pexpr α] :
α → pexpr
source
@[protected, instance]
meta def pexpr.has_to_pexpr  :
has_to_pexpr pexpr
source
@[protected, instance]
meta def expr.has_to_pexpr  :
has_to_pexpr expr
source
@[protected, instance]
meta def reflected.has_to_pexpr (α : Sort u) (a : α) :
has_to_pexpr (reflected α a)