mathlib documentation

core / init.meta.tagged_format

meta inductive tagged_format (α : Type u) :
Type u

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

meta def tagged_format.map {α β : Type u} (f : α → β) :

meta def tagged_format.m_untag {α : Type u} {t : Type → Type} [monad t] (f : α → formatt format) :

meta def tagged_format.untag {α : Type u} (f : α → formatformat) :

@[instance]
meta def tagged_format.has_to_fmt {α : Type u} :

meta def eformat  :
Type

tagged_format with information about subexpressions.

meta constant tactic_state.pp_tagged  :

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.