def
Lean.Server.Completion.find?
(params : Lsp.CompletionParams)
(fileMap : FileMap)
(hoverPos : String.Pos)
(cmdStx : Syntax)
(infoTree : Elab.InfoTree)
(caps : Lsp.ClientCapabilities)
:
Equations
- One or more equations did not get rendered due to their size.