- 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.
def
tagged_format.m_untag
{α : Type u}
{t : Type → Type}
[monad t] :
(α → format → t format) → tagged_format α → t format
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.