def Lapis.Server.InlayHints.labelString (label : String) : Lean.Json

Build an inlay hint label from a plain string

Equations

• Lapis.Server.InlayHints.labelString label = Lean.Json.str label

def Lapis.Server.InlayHints.labelParts (parts : Array Protocol.Generated.InlayHintLabelPart) : Lean.Json

Build an inlay hint label from label parts

Equations

• Lapis.Server.InlayHints.labelParts parts = Lean.toJson parts

structure Lapis.Server.InlayHints.InlayHintBuilder : Type

Builder for collecting inlay hints

• hints : Array Protocol.Generated.InlayHint

@[implicit_reducible]

instance Lapis.Server.InlayHints.instInhabitedInlayHintBuilder : Inhabited InlayHintBuilder

Equations

• Lapis.Server.InlayHints.instInhabitedInlayHintBuilder = { default := Lapis.Server.InlayHints.instInhabitedInlayHintBuilder.default }

def Lapis.Server.InlayHints.instInhabitedInlayHintBuilder.default : InlayHintBuilder

Equations

• Lapis.Server.InlayHints.instInhabitedInlayHintBuilder.default = { hints := default }

def Lapis.Server.InlayHints.InlayHintBuilder.new : InlayHintBuilder

Create a new inlay hint builder

Equations

• Lapis.Server.InlayHints.InlayHintBuilder.new = { }

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) : InlayHintBuilder

Add an inlay hint with a raw JSON label

Equations

• One or more equations did not get rendered due to their size.

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) : InlayHintBuilder

Add an inlay hint with a string label

Equations

• One or more equations did not get rendered due to their size.

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) : InlayHintBuilder

Add an inlay hint with label parts

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.InlayHints.InlayHintBuilder.build (b : InlayHintBuilder) : Array Protocol.Generated.InlayHint

Build the inlay hint array

Equations

• b.build = b.hints

def Lapis.Server.InlayHints.InlayHintBuilder.isEmpty (b : InlayHintBuilder) : Bool

Check if the builder has any hints

Equations

• b.isEmpty = b.hints.isEmpty

def Lapis.Server.InlayHints.InlayHintBuilder.size (b : InlayHintBuilder) : Nat

Get the number of hints

Equations

• b.size = b.hints.size