inductive Lean.Widget.TaggedText (α : Type u) :

The minimal structure needed to represent "string with interesting (tagged) substrings". Much like Lean 3 sf, but with indentation already stringified.

Instances For
    instance Lean.Widget.instBEqTaggedText :
    {α : Type u_1} → [inst : BEq α] → BEq (Lean.Widget.TaggedText α)
    instance Lean.Widget.instReprTaggedText :
    {α : Type u_1} → [inst : Repr α] → Repr (Lean.Widget.TaggedText α)
    partial def {α : Type u_1} {β : Type u_2} (f : αβ) :
    partial def Lean.Widget.TaggedText.mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : αm β) :
    partial def Lean.Widget.TaggedText.rewriteM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : αLean.Widget.TaggedText αm (Lean.Widget.TaggedText β)) :

    Like mapM but allows rewriting the whole subtree at tag nodes.

    The output is tagged with (tag, indent) where tag is from the input Format and indent is the indentation level at this point. The latter is used to print sub-trees accurately by passing it again as the indent argument.

    Instances For

      Remove tags, leaving just the pretty-printed string.

      Instances For