mathlib3 documentation

core / init.meta.tagged_format

meta inductive tagged_format (α : Type u) :

An alternative to format that keeps structural information stored as a tag.

Instances for tagged_format
meta def {α β : Type u} (f : α β) :
@[protected, instance]
meta def tagged_format.m_untag {α : Type u} {t : Type Type} [monad t] (f : α format t format) :
@[protected, instance]
meta def eformat  :

tagged_format with information about subexpressions.

A special version of pp which also preserves expression boundary information.

On a tag ⟨e,a⟩, note that the given expr e is not necessarily the subexpression of the root expression that tactic_state.pp_tagged was called with. For example if the subexpression is under a binder then all of the expr.var 0s will be replaced with a local constant not in the local context with the name and type set to that of the binder.