Documentation

Lean.Server.Completion.CompletionCollectors

source
def Lean.Server.Completion.idCompletion (uri : Lsp.DocumentUri) (pos : Lsp.Position) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (lctx : LocalContext) (stx : Syntax) (id : Name) (hoverInfo : HoverInfo) (danglingDot : Bool) :
CancellableM (Array Lsp.ResolvableCompletionItem)
Instances For
    source
    def Lean.Server.Completion.dotCompletion (uri : Lsp.DocumentUri) (pos : Lsp.Position) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (info : Elab.TermInfo) :
    CancellableM (Array Lsp.ResolvableCompletionItem)
    Instances For
      source
      def Lean.Server.Completion.dotIdCompletion (uri : Lsp.DocumentUri) (pos : Lsp.Position) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (lctx : LocalContext) (id : Name) (expectedType? : Option Expr) :
      CancellableM (Array Lsp.ResolvableCompletionItem)
      Instances For
        source
        def Lean.Server.Completion.fieldIdCompletion (uri : Lsp.DocumentUri) (pos : Lsp.Position) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (lctx : LocalContext) (id : Option Name) (structName : Name) :
        CancellableM (Array Lsp.ResolvableCompletionItem)
        Instances For
          source
          def Lean.Server.Completion.optionCompletion (uri : Lsp.DocumentUri) (pos : Lsp.Position) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (stx : Syntax) (caps : Lsp.ClientCapabilities) :
          IO (Array Lsp.ResolvableCompletionItem)
          Instances For
            source
            def Lean.Server.Completion.errorNameCompletion (uri : Lsp.DocumentUri) (pos : Lsp.Position) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (partialId : Syntax) (caps : Lsp.ClientCapabilities) :
            IO (Array Lsp.ResolvableCompletionItem)
            Instances For
              source
              def Lean.Server.Completion.tacticCompletion (uri : Lsp.DocumentUri) (pos : Lsp.Position) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) :
              IO (Array Lsp.ResolvableCompletionItem)
              Instances For
                source
                def Lean.Server.Completion.endSectionCompletion (uri : Lsp.DocumentUri) (pos : Lsp.Position) (completionInfoPos : Nat) (id? : Option Name) (danglingDot : Bool) (scopeNames : List String) :
                IO (Array Lsp.ResolvableCompletionItem)
                Instances For