Documentation

Lean.Server.Completion.CompletionCollectors

source
def Lean.Server.Completion.idCompletion (params : Lsp.CompletionParams) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (lctx : LocalContext) (stx : Syntax) (id : Name) (hoverInfo : HoverInfo) (danglingDot : Bool) :
CancellableM (Array Lsp.CompletionItem)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Server.Completion.dotCompletion (params : Lsp.CompletionParams) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (info : Elab.TermInfo) :
    CancellableM (Array Lsp.CompletionItem)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Server.Completion.dotIdCompletion (params : Lsp.CompletionParams) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (lctx : LocalContext) (id : Name) (expectedType? : Option Expr) :
      CancellableM (Array Lsp.CompletionItem)
      Instances For
        source
        def Lean.Server.Completion.fieldIdCompletion (params : Lsp.CompletionParams) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (lctx : LocalContext) (id : Option Name) (structName : Name) :
        CancellableM (Array Lsp.CompletionItem)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Server.Completion.optionCompletion (params : Lsp.CompletionParams) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (stx : Syntax) (caps : Lsp.ClientCapabilities) :
          IO (Array Lsp.CompletionItem)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Server.Completion.errorNameCompletion (params : Lsp.CompletionParams) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (partialId : Syntax) (caps : Lsp.ClientCapabilities) :
            IO (Array Lsp.CompletionItem)
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Lean.Server.Completion.tacticCompletion (params : Lsp.CompletionParams) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) :
              IO (Array Lsp.CompletionItem)
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For