mathlib documentation

core.init.meta.pexpr

meta def pexpr  :
Type

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

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.

meta def to_pexpr {α : Sort u} [has_to_pexpr α] :
α → pexpr

@[instance]

@[instance]

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