Documentation

Lean.Server.CodeActions.UnknownIdentifier

source
def Lean.Server.FileWorker.waitUnknownIdentifierRanges (doc : EditableDocument) (requestedRange : Syntax.Range) :
BaseIO (Array Syntax.Range × Bool)
Instances For
    source
    def Lean.Server.FileWorker.waitAllUnknownIdentifierMessageRanges (doc : EditableDocument) :
    BaseIO (Array Syntax.Range)
    Instances For
      source
      structure Lean.Server.FileWorker.Insertion :
      Type
      Instances For
        source
        structure Lean.Server.FileWorker.Queryextends Lean.Lsp.LeanModuleQuery :
        Type
        Instances For
          source
          def Lean.Server.FileWorker.collectOpenNamespaces (currentNamespace : Name) (openDecls : List OpenDecl) :
          Array Lsp.OpenNamespace
          Instances For
            source
            def Lean.Server.FileWorker.computeIdQuery? (doc : EditableDocument) (ctx : Elab.ContextInfo) (stx : Syntax) (id : Name) :
            Option Query
            Instances For
              source
              def Lean.Server.FileWorker.computeDotQuery? (doc : EditableDocument) (ctx : Elab.ContextInfo) (ti : Elab.TermInfo) :
              IO (Option Query)
              Instances For
                source
                def Lean.Server.FileWorker.computeDotIdQuery? (doc : EditableDocument) (ctx : Elab.ContextInfo) (stx : Syntax) (id : Name) (lctx : LocalContext) (expectedType? : Option Expr) :
                IO (Option Query)
                Instances For
                  source
                  def Lean.Server.FileWorker.computeQueries (doc : EditableDocument) (requestedPos : String.Pos.Raw) :
                  RequestM (Array Query)
                  Instances For
                    source
                    def Lean.Server.FileWorker.importAllUnknownIdentifiersProvider :
                    Name
                    Instances For
                      source
                      def Lean.Server.FileWorker.importUnknownIdentifiersProvider :
                      Name
                      Instances For
                        source
                        def Lean.Server.FileWorker.mkUnknownIdentifierCodeActionData (params : Lsp.CodeActionParams) (name : Name := importUnknownIdentifiersProvider) :
                        CodeActionResolveData
                        Instances For
                          source
                          def Lean.Server.FileWorker.importAllUnknownIdentifiersCodeAction (params : Lsp.CodeActionParams) (kind : String) :
                          Lsp.CodeAction
                          Instances For
                            source
                            def Lean.Server.FileWorker.handleUnknownIdentifierCodeAction (id : JsonRpc.RequestID) (params : Lsp.CodeActionParams) (requestedRange : Syntax.Range) (kind : String) :
                            RequestM (Array Lsp.CodeAction)
                            Instances For
                              source
                              def Lean.Server.FileWorker.handleResolveImportAllUnknownIdentifiersCodeAction? (id : JsonRpc.RequestID) (action : Lsp.CodeAction) (unknownIdentifierRanges : Array Syntax.Range) :
                              RequestM (Option Lsp.CodeAction)
                              Instances For