mathlib documentation

core / init.meta.pexpr

@[reducible]
meta def pexpr  :
Type

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

@[protected]
meta constant pexpr.of_expr  :
meta constant pexpr.is_placeholder  :
meta constant pexpr.mk_placeholder  :
meta constant pexpr.mk_field_macro  :
pexprnamepexpr
meta constant pexpr.mk_explicit  :
meta constant pexpr.is_choice_macro  :

Choice macros are used to implement overloading.

meta structure structure_instance_info  :
Type

Information about unelaborated structure instance expressions.

Create a structure instance expression.

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