- text: {α : Type u} → String → Lean.Widget.TaggedText α
- append: {α : Type u} → Array (Lean.Widget.TaggedText α) → Lean.Widget.TaggedText α
- tag: {α : Type u} → α → Lean.Widget.TaggedText α → Lean.Widget.TaggedText α
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 α)
instance
Lean.Widget.instFromJsonTaggedText :
{α : Type} → [inst : Lean.FromJson α] → Lean.FromJson (Lean.Widget.TaggedText α)
instance
Lean.Widget.instToJsonTaggedText :
{α : Type u_1} → [inst : Lean.ToJson α] → Lean.ToJson (Lean.Widget.TaggedText α)
Instances For
def
Lean.Widget.TaggedText.appendTag
{α : Type u_1}
(acc : Lean.Widget.TaggedText α)
(t₀ : α)
(a₀ : Lean.Widget.TaggedText α)
:
Instances For
partial def
Lean.Widget.TaggedText.mapM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
(f : α → m β)
:
Lean.Widget.TaggedText α → m (Lean.Widget.TaggedText β)
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_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
(f : α → Lean.Widget.TaggedText α → m (Lean.Widget.TaggedText β))
:
Lean.Widget.TaggedText α → m (Lean.Widget.TaggedText β)
Like mapM
but allows rewriting the whole subtree at tag
nodes.
def
Lean.Widget.TaggedText.prettyTagged
(f : Lean.Format)
(indent : optParam Nat 0)
(w : optParam Nat Std.Format.defWidth)
:
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.