Build an inlay hint label from a plain string
Equations
- Lapis.Server.InlayHints.labelString label = Lean.Json.str label
Instances For
Build an inlay hint label from label parts
Equations
- Lapis.Server.InlayHints.labelParts parts = Lean.toJson parts
Instances For
@[implicit_reducible]
Equations
Instances For
Create a new inlay hint builder
Equations
Instances For
def
Lapis.Server.InlayHints.InlayHintBuilder.push
(b : InlayHintBuilder)
(position : Protocol.Generated.Position)
(label : Lean.Json)
(kind : Option Protocol.Generated.InlayHintKind := none)
(tooltip : Option String := none)
(textEdits : Option (Array Protocol.Generated.TextEdit) := none)
(paddingLeft paddingRight : Option Bool := none)
(data : Option Lean.Json := none)
:
Add an inlay hint with a raw JSON label
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lapis.Server.InlayHints.InlayHintBuilder.pushStringLabel
(b : InlayHintBuilder)
(position : Protocol.Generated.Position)
(label : String)
(kind : Option Protocol.Generated.InlayHintKind := none)
(tooltip : Option String := none)
(textEdits : Option (Array Protocol.Generated.TextEdit) := none)
(paddingLeft paddingRight : Option Bool := none)
(data : Option Lean.Json := none)
:
Add an inlay hint with a string label
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lapis.Server.InlayHints.InlayHintBuilder.pushLabelParts
(b : InlayHintBuilder)
(position : Protocol.Generated.Position)
(parts : Array Protocol.Generated.InlayHintLabelPart)
(kind : Option Protocol.Generated.InlayHintKind := none)
(tooltip : Option String := none)
(textEdits : Option (Array Protocol.Generated.TextEdit) := none)
(paddingLeft paddingRight : Option Bool := none)
(data : Option Lean.Json := none)
:
Add an inlay hint with label parts
Equations
- One or more equations did not get rendered due to their size.
Instances For
Build the inlay hint array
Instances For
Check if the builder has any hints
Instances For
Get the number of hints