@[reducible, inline]

abbrev ImportCompletion.ImportTrie : Type

Equations

• ImportCompletion.ImportTrie = Lean.NameTrie Lean.Name

@[reducible, inline]

abbrev ImportCompletion.AvailableImports : Type

Equations

• ImportCompletion.AvailableImports = Array Lean.Name

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

Equations

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

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

Checks whether completionPos points at the position after an incomplete import statement.

Equations

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

def ImportCompletion.isImportCmdCompletionRequest (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (completionPos : String.Pos) : 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 ImportCompletion.computePartialImportCompletions (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (completionPos : String.Pos) (availableImports : ImportTrie) : Array Lean.Name

Equations

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

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

Equations

• ImportCompletion.isImportCompletionRequest text headerStx params = decide (text.lspPosToUtf8Pos params.position ≤ headerStx.raw.getTailPos?.getD (headerStx.raw.getPos?.getD 0) + ' ' + ' ')

def ImportCompletion.collectAvailableImportsFromLake : IO (Option AvailableImports)

Equations

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

def ImportCompletion.collectAvailableImportsFromSrcSearchPath : IO AvailableImports

Equations

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

def ImportCompletion.collectAvailableImports : IO AvailableImports

Equations

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

def ImportCompletion.addCompletionItemData (completionList : Lean.Lsp.CompletionList) (params : Lean.Lsp.CompletionParams) : Lean.Lsp.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 ImportCompletion.find (text : Lean.FileMap) (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (params : Lean.Lsp.CompletionParams) (availableImports : AvailableImports) : Lean.Lsp.CompletionList

Equations

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

def ImportCompletion.computeCompletions (text : Lean.FileMap) (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (params : Lean.Lsp.CompletionParams) : IO Lean.Lsp.CompletionList

Equations

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