The minimal structure needed to represent "string with interesting (tagged) substrings".
Much like Lean 3 sf
,
but with indentation already stringified.
- text {α : Type u} : String → TaggedText α
- append {α : Type u} : Array (TaggedText α) → TaggedText α
- tag {α : Type u} : α → TaggedText α → TaggedText α
Instances For
Equations
Instances For
partial def
Lean.Widget.instBEqTaggedText.beq
{α✝ : Type u_1}
[BEq α✝]
:
TaggedText α✝ → TaggedText α✝ → Bool
Equations
partial def
Lean.Widget.instReprTaggedText.repr
{α✝ : Type u_1}
[Repr α✝]
:
TaggedText α✝ → Nat → Format
Equations
partial def
Lean.Widget.instFromJsonTaggedText.fromJson
{α✝ : Type}
[FromJson α✝]
:
Json → Except String (TaggedText α✝)
Equations
Equations
partial def
Lean.Widget.instToJsonTaggedText.toJson
{α✝ : Type u_1}
[ToJson α✝]
:
TaggedText α✝ → Json
Equations
- One or more equations did not get rendered due to their size.
- Lean.Widget.TaggedText.appendText s₀ (Lean.Widget.TaggedText.text s) = Lean.Widget.TaggedText.text (s ++ s₀)
- Lean.Widget.TaggedText.appendText s₀ x✝ = Lean.Widget.TaggedText.append #[x✝, Lean.Widget.TaggedText.text s₀]
Instances For
def
Lean.Widget.TaggedText.appendTag
{α : Type u_1}
(acc : TaggedText α)
(t₀ : α)
(a₀ : TaggedText α)
:
Equations
- (Lean.Widget.TaggedText.append as).appendTag t₀ a₀ = Lean.Widget.TaggedText.append (as.push (Lean.Widget.TaggedText.tag t₀ a₀))
- (Lean.Widget.TaggedText.text "").appendTag t₀ a₀ = Lean.Widget.TaggedText.tag t₀ a₀
- acc.appendTag t₀ a₀ = Lean.Widget.TaggedText.append #[acc, Lean.Widget.TaggedText.tag t₀ a₀]
Instances For
partial def
Lean.Widget.TaggedText.map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
:
TaggedText α → TaggedText β
partial def
Lean.Widget.TaggedText.mapM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
(f : α → m β)
:
TaggedText α → m (TaggedText β)
partial def
Lean.Widget.TaggedText.rewrite
{α : Type u_1}
{β : Type u_2}
(f : α → TaggedText α → TaggedText β)
:
TaggedText α → TaggedText β
partial def
Lean.Widget.TaggedText.rewriteM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
(f : α → TaggedText α → m (TaggedText β))
:
TaggedText α → m (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.
def
Lean.Widget.TaggedText.prettyTagged
(f : Format)
(indent : Nat := 0)
(w : Nat := Std.Format.defWidth)
:
TaggedText (Nat × Nat)
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 = Lean.Widget.TaggedText.TaggedState.out✝ (f.prettyM w indent { }).snd
Instances For
Remove tags, leaving just the pretty-printed string.