Documentation

Lean.Widget.TaggedText

inductive Lean.Widget.TaggedText (α : Type u) :
Type u
instance Lean.Widget.instToJsonTaggedText :
{α : Type u_1} → [inst : Lean.ToJson α] → Lean.ToJson (Lean.Widget.TaggedText α)
Equations
  • Lean.Widget.instToJsonTaggedText = { toJson := [anonymous] }
instance Lean.Widget.instReprTaggedText :
{α : Type u_1} → [inst : Repr α] → Repr (Lean.Widget.TaggedText α)
Equations
  • Lean.Widget.instReprTaggedText = { reprPrec := [anonymous] }
Equations
  • Lean.Widget.instFromJsonTaggedText = { fromJson? := [anonymous] }
Equations
instance Lean.Widget.instBEqTaggedText :
{α : Type u_1} → [inst : BEq α] → BEq (Lean.Widget.TaggedText α)
Equations
  • Lean.Widget.instBEqTaggedText = { beq := [anonymous] }
partial def Lean.Widget.TaggedText.map {α : Type u_1} {β : Type u_2} (f : αβ) :
partial def Lean.Widget.TaggedText.mapM {m : Type u_1Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : αm β) :
partial def Lean.Widget.TaggedText.rewrite {α : Type u_1} {β : Type u_2} (f : αLean.Widget.TaggedText αLean.Widget.TaggedText β) :
partial def Lean.Widget.TaggedText.rewriteM {m : Type u_1Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : αLean.Widget.TaggedText αm (Lean.Widget.TaggedText β)) :
Equations
Equations
Equations
Equations
partial def Lean.Widget.TaggedText.stripTags.go {α : Type u_1} (acc : String) :