def
Lean.Server.FileWorker.SignatureHelp.determineSignatureHelp
(tree : Elab.InfoTree)
(appStx : Syntax)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
- pipeArg : CandidateKind
Cursor is in the position of the argument to a pipe, like
<|
or$
. Low precedence. Ensures thatfun <| otherFun <cursor>
yields the signature help ofotherFun
, notfun
. - termArg : CandidateKind
Cursor is in the position of the trailing whitespace of some term. Medium precedence. Ensures that
fun otherFun <cursor>
yields the signature help offun
, nototherFun
. - appArg : CandidateKind
Cursor is in the position of the argument to a function that already has other arguments applied to it. High precedence.
Instances For
Equations
Instances For
- kind : CandidateKind
- appStx : Syntax
Instances For
- continue : SearchControl
In a syntax stack, keep searching upwards, continuing with the parent of the current term.
- stop : SearchControl
Stop the search through a syntax stack.
Instances For
def
Lean.Server.FileWorker.SignatureHelp.findSignatureHelp?
(text : FileMap)
(ctx? : Option Lsp.SignatureHelpContext)
(cmdStx : Syntax)
(tree : Elab.InfoTree)
(requestedPos : String.Pos)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Server.FileWorker.SignatureHelp.findSignatureHelp?.determineCandidateKind
(text : FileMap)
(ctx? : Option Lsp.SignatureHelpContext)
(requestedPos : String.Pos)
(stx parent : Syntax)
:
Equations
- One or more equations did not get rendered due to their size.