@[reducible, inline]

abbrev Lean.Lsp.ImportCompletion.ImportTrie : Type

Equations

• Lean.Lsp.ImportCompletion.ImportTrie = Lean.NameTrie Lean.Name

@[reducible, inline]

abbrev Lean.Lsp.ImportCompletion.AvailableImports : Type

Equations

• Lean.Lsp.ImportCompletion.AvailableImports = Array Lean.Name

def Lean.Lsp.ImportCompletion.AvailableImports.toImportTrie (imports : AvailableImports) : ImportTrie

Equations

• One or more equations did not get rendered due to their size.

def Lean.Lsp.ImportCompletion.isImportNameCompletionRequest (headerStx : TSyntax `Lean.Parser.Module.header) (completionPos : String.Pos.Raw) : Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.Lsp.ImportCompletion.isImportCmdCompletionRequest (headerStx : TSyntax `Lean.Parser.Module.header) (completionPos : String.Pos.Raw) : Bool

Checks whether completionPos points at a free space in the header.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Lsp.ImportCompletion.computePartialImportCompletions (headerStx : TSyntax `Lean.Parser.Module.header) (completionPos : String.Pos.Raw) (availableImports : ImportTrie) : Array Name

Equations

• One or more equations did not get rendered due to their size.

def Lean.Lsp.ImportCompletion.isImportCompletionRequest (text : FileMap) (headerStx : TSyntax `Lean.Parser.Module.header) (params : CompletionParams) : Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.Lsp.ImportCompletion.collectAvailableImportsFromLake : IO (Option AvailableImports)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Lsp.ImportCompletion.collectAvailableImportsFromSrcSearchPath : IO AvailableImports

Equations

• One or more equations did not get rendered due to their size.

def Lean.Lsp.ImportCompletion.collectAvailableImports : IO AvailableImports

Equations

• One or more equations did not get rendered due to their size.

def Lean.Lsp.ImportCompletion.addCompletionItemData (uri : DocumentUri) (pos : Position) (completionList : CompletionList) : CompletionList

Sets the data? field of every CompletionItem in completionList using params. Ensures that completionItem/resolve requests can be routed to the correct file worker even for CompletionItems produced by the import completion.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Lsp.ImportCompletion.find (uri : DocumentUri) (pos : Position) (text : FileMap) (headerStx : TSyntax `Lean.Parser.Module.header) (availableImports : AvailableImports) : CompletionList

Equations

• One or more equations did not get rendered due to their size.

def Lean.Lsp.ImportCompletion.computeCompletions (uri : DocumentUri) (pos : Position) (text : FileMap) (headerStx : TSyntax `Lean.Parser.Module.header) : IO CompletionList

Equations

• One or more equations did not get rendered due to their size.