def
Lean.Server.Completion.find?
(mod : Name)
(pos : Lsp.Position)
(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.