TorchLean API

Docs HomeGuideExamplesGraphs

Lean.Server.FileWorker.InlayHints

source
def Lean.Elab.InlayHintLinkLocation.toLspLocation (text : FileMap) (l : InlayHintLinkLocation) :
IO (Option Lsp.Location)
Instances For
    source
    def Lean.Elab.InlayHintLabelPart.toLspInlayHintLabelPart (text : FileMap) (p : InlayHintLabelPart) :
    IO Lsp.InlayHintLabelPart
    Instances For
      source
      def Lean.Elab.InlayHintLabel.toLspInlayHintLabel (text : FileMap) :
      InlayHintLabel → IO Lsp.InlayHintLabel
      Instances For
        source
        def Lean.Elab.InlayHintKind.toLspInlayHintKind :
        InlayHintKind → Lsp.InlayHintKind
        Instances For
          source
          def Lean.Elab.InlayHintTextEdit.toLspTextEdit (text : FileMap) (e : InlayHintTextEdit) :
          Lsp.TextEdit
          Instances For
            source
            def Lean.Elab.InlayHintInfo.toLspInlayHint (text : FileMap) (i : InlayHintInfo) :
            IO Lsp.InlayHint
            Instances For
              source
              def Lean.Server.FileWorker.applyEditToHint? (hintMod : Name) (ihi : Elab.InlayHintInfo) (range : Syntax.Range) (newText : String) :
              Option Elab.InlayHintInfo
              Instances For
                source
                structure Lean.Server.FileWorker.InlayHintState :
                Type
                Instances For
                  source
                  @[implicit_reducible]
                  instance Lean.Server.FileWorker.instTypeNameInlayHintState :
                  TypeName InlayHintState
                  source
                  def Lean.Server.FileWorker.instInhabitedInlayHintState.default :
                  InlayHintState
                  Instances For
                    source
                    @[implicit_reducible]
                    instance Lean.Server.FileWorker.instInhabitedInlayHintState :
                    Inhabited InlayHintState
                    source
                    def Lean.Server.FileWorker.InlayHintState.init :
                    InlayHintState
                    Instances For
                      source
                      def Lean.Server.FileWorker.handleInlayHints (p : Lsp.InlayHintParams) (s : InlayHintState) :
                      RequestM (LspResponse (Array Lsp.InlayHint) × InlayHintState)
                      Instances For
                        source
                        def Lean.Server.FileWorker.handleInlayHintsDidChange (p : Lsp.DidChangeTextDocumentParams) :
                        StateT InlayHintState RequestM Unit
                        Instances For