def Lean.Elab.InlayHintLinkLocation.toLspLocation (text : FileMap) (l : InlayHintLinkLocation) : IO (Option Lsp.Location)

Equations

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

def Lean.Elab.InlayHintLabelPart.toLspInlayHintLabelPart (text : FileMap) (p : InlayHintLabelPart) : IO Lsp.InlayHintLabelPart

Equations

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

def Lean.Elab.InlayHintLabel.toLspInlayHintLabel (text : FileMap) : InlayHintLabel → IO Lsp.InlayHintLabel

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.InlayHintLabel.toLspInlayHintLabel text (Lean.Elab.InlayHintLabel.name n) = pure (Lean.Lsp.InlayHintLabel.name n)

def Lean.Elab.InlayHintKind.toLspInlayHintKind : InlayHintKind → Lsp.InlayHintKind

Equations

• Lean.Elab.InlayHintKind.type.toLspInlayHintKind = Lean.Lsp.InlayHintKind.type
• Lean.Elab.InlayHintKind.parameter.toLspInlayHintKind = Lean.Lsp.InlayHintKind.parameter

def Lean.Elab.InlayHintTextEdit.toLspTextEdit (text : FileMap) (e : InlayHintTextEdit) : Lsp.TextEdit

Equations

• Lean.Elab.InlayHintTextEdit.toLspTextEdit text e = { range := text.utf8RangeToLspRange e.range, newText := e.newText }

def Lean.Elab.InlayHintInfo.toLspInlayHint (text : FileMap) (i : InlayHintInfo) : IO Lsp.InlayHint

Equations

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

def Lean.Server.FileWorker.applyEditToHint? (hintMod : Name) (ihi : Elab.InlayHintInfo) (range : String.Range) (newText : String) : Option Elab.InlayHintInfo

Equations

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

structure Lean.Server.FileWorker.InlayHintState : Type

• oldInlayHints : Array Elab.InlayHintInfo
• oldFinishedSnaps : Nat
• lastEditTimestamp? : Option Nat
• isFirstRequestAfterEdit : Bool

instance Lean.Server.FileWorker.instTypeNameInlayHintState : TypeName InlayHintState

Equations

• Lean.Server.FileWorker.instTypeNameInlayHintState = Lean.Server.FileWorker.inst✝

instance Lean.Server.FileWorker.instInhabitedInlayHintState : Inhabited InlayHintState

Equations

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

def Lean.Server.FileWorker.InlayHintState.init : InlayHintState

Equations

• Lean.Server.FileWorker.InlayHintState.init = { oldInlayHints := #[], oldFinishedSnaps := 0, lastEditTimestamp? := none, isFirstRequestAfterEdit := false }

def Lean.Server.FileWorker.handleInlayHints (p : Lsp.InlayHintParams) (s : InlayHintState) : RequestM (LspResponse (Array Lsp.InlayHint) × InlayHintState)

Equations

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

def Lean.Server.FileWorker.handleInlayHintsDidChange (p : Lsp.DidChangeTextDocumentParams) : StateT InlayHintState RequestM Unit

Equations

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

def Lean.Server.FileWorker.handleInlayHintsDidChange.updateOldInlayHints (p : Lsp.DidChangeTextDocumentParams) (oldInlayHints : Array Elab.InlayHintInfo) : RequestM (Array Elab.InlayHintInfo)

Equations

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

def Lean.Server.FileWorker.handleInlayHintsDidChange.determineLastEditTimestamp? (p : Lsp.DidChangeTextDocumentParams) (oldInlayHints : Array Elab.InlayHintInfo) : RequestM (Option Nat)

Equations

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