mathlib documentation


meta inductive tagged_format  :
Type uType u

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

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

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

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

meta def tagged_format.has_to_fmt {α : Type u} :

meta def eformat  :

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.