Documentation

Lean.Server.Completion.ImportCompletion

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

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

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

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.