Equations
Instances For
def
Lean.Elab.InlayHintLabelPart.toLspInlayHintLabelPart
(text : FileMap)
(p : InlayHintLabelPart)
:
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
def
Lean.Server.FileWorker.applyEditToHint?
(hintMod : Name)
(ihi : Elab.InlayHintInfo)
(range : String.Range)
(newText : String)
:
Equations
Instances For
- oldInlayHints : Array Elab.InlayHintInfo
- oldFinishedSnaps : Nat
- isFirstRequestAfterEdit : Bool
Instances For
Equations
Equations
Instances For
Equations
Instances For
def
Lean.Server.FileWorker.handleInlayHintsDidChange.updateOldInlayHints
(p : Lsp.DidChangeTextDocumentParams)
(oldInlayHints : Array Elab.InlayHintInfo)
:
Equations
Instances For
def
Lean.Server.FileWorker.handleInlayHintsDidChange.determineLastEditTimestamp?
(p : Lsp.DidChangeTextDocumentParams)
(oldInlayHints : Array Elab.InlayHintInfo)
: