mathlib3 documentation

core / init.meta.tagged_format

meta inductive tagged_format (α : Type u) :

tag : Π {α : Type u}, α → tagged_format α → tagged_format α
compose : Π {α : Type u}, tagged_format α → tagged_format α → tagged_format α
group : Π {α : Type u}, tagged_format α → tagged_format α
nest : Π {α : Type u}, ℕ → tagged_format α → tagged_format α
highlight : Π {α : Type u}, format.color → tagged_format α → tagged_format α
of_format : Π {α : Type u}, format → tagged_format α

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

Instances for tagged_format

@[protected]

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

tagged_format α → tagged_format β

@[protected, instance]

meta def tagged_format.is_functor :

functor tagged_format

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

tagged_format α → t format

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

tagged_format α → format

@[protected, instance]

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

has_to_format (tagged_format α)

meta def eformat :

tagged_format with information about subexpressions.

meta constant tactic_state.pp_tagged :

tactic_state → expr → eformat

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.

meta def tactic.pp_tagged :

expr → tactic eformat