Documentation

Lean.Widget.TaggedText

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
    Equations
    instance Lean.Widget.instBEqTaggedText :
    {α : Type u_1} → [inst : BEq α] → BEq (Lean.Widget.TaggedText α)
    Equations
    • Lean.Widget.instBEqTaggedText = { beq := Lean.Widget.beqTaggedText✝ }
    instance Lean.Widget.instReprTaggedText :
    {α : Type u_1} → [inst : Repr α] → Repr (Lean.Widget.TaggedText α)
    Equations
    • Lean.Widget.instReprTaggedText = { reprPrec := Lean.Widget.reprTaggedText✝ }
    Equations
    • Lean.Widget.instFromJsonTaggedText = { fromJson? := Lean.Widget.fromJsonTaggedText✝ }
    Equations
    • Lean.Widget.instToJsonTaggedText = { toJson := Lean.Widget.toJsonTaggedText✝ }
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        partial def Lean.Widget.TaggedText.map {α : 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.

        Equations
        • One or more equations did not get rendered due to their size.
        Equations

        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.

        Equations
        Instances For

          Remove tags, leaving just the pretty-printed string.

          Equations
          Instances For