mathlib documentation

core.init.meta.pexpr

source
meta def pexpr  :
Type

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

source
meta constant pexpr.of_expr (a : expr) :
pexpr

source
meta constant pexpr.is_placeholder (a : pexpr) :
bool

source
meta constant pexpr.mk_placeholder  :
pexpr

source
meta constant pexpr.mk_field_macro (a : pexpr) (a_1 : name) :
pexpr

source
meta constant pexpr.mk_explicit (a : pexpr) :
pexpr

source
meta constant pexpr.is_choice_macro (a : 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 (a : structure_instance_info) :
pexpr

Create a structure instance expression.

source
meta constant pexpr.get_structure_instance_info (a : pexpr) :
option structure_instance_info

source
@[class]
meta structure has_to_pexpr (α : Sort u) :
Sort (max 1 u)
  • to_pexpr : α → pexpr

Instances
source
meta def to_pexpr {α : Sort u} [has_to_pexpr α] (a : α) :
pexpr

source
@[instance]
meta def pexpr.has_to_pexpr  :
has_to_pexpr pexpr

source
@[instance]
meta def expr.has_to_pexpr  :
has_to_pexpr expr

source
@[instance]
meta def reflected.has_to_pexpr (α : Sort u) (a : α) :
has_to_pexpr (reflected a)