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