- 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.
Equations
- Lean.Widget.instInhabitedTaggedText = { default := Lean.Widget.TaggedText.text default }
instance
Lean.Widget.instBEqTaggedText:
{α : Type u_1} → [inst : BEq α] → BEq (Lean.Widget.TaggedText α)
Equations
- Lean.Widget.instBEqTaggedText = { beq := [anonymous] }
instance
Lean.Widget.instReprTaggedText:
{α : Type u_1} → [inst : Repr α] → Repr (Lean.Widget.TaggedText α)
Equations
- Lean.Widget.instReprTaggedText = { reprPrec := [anonymous] }
instance
Lean.Widget.instFromJsonTaggedText:
{α : Type} → [inst : Lean.FromJson α] → Lean.FromJson (Lean.Widget.TaggedText α)
Equations
- Lean.Widget.instFromJsonTaggedText = { fromJson? := [anonymous] }
instance
Lean.Widget.instToJsonTaggedText:
{α : Type u_1} → [inst : Lean.ToJson α] → Lean.ToJson (Lean.Widget.TaggedText α)
Equations
- Lean.Widget.instToJsonTaggedText = { toJson := [anonymous] }
Equations
- One or more equations did not get rendered due to their size.
def
Lean.Widget.TaggedText.appendTag
{α : Type u_1}
(acc : Lean.Widget.TaggedText α)
(t₀ : α)
(a₀ : Lean.Widget.TaggedText α)
:
Equations
- One or more equations did not get rendered due to their size.
partial def
Lean.Widget.TaggedText.mapM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[inst : 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}
[inst : 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.
instance
Lean.Widget.TaggedText.instRpcEncodingTaggedText
{α : Type}
{β : Type}
[inst : Lean.Server.RpcEncoding α β]
:
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Widget.TaggedText.instInhabitedTaggedState = { default := { out := default, tagStack := default, column := default } }
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- Lean.Widget.TaggedText.prettyTagged f indent w = (Std.Format.prettyM f w indent { out := Lean.Widget.TaggedText.text "", tagStack := [], column := 0 }).snd.out
Remove tags, leaving just the pretty-printed string.