def Lean.Server.FileWorker.SignatureHelp.determineSignatureHelp (tree : Elab.InfoTree) (appStx : Syntax) : IO (Option Lsp.SignatureHelp)

Equations

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

inductive Lean.Server.FileWorker.SignatureHelp.CandidateKind : Type

• pipeArg : CandidateKind

  Cursor is in the position of the argument to a pipe, like <| or $. Low precedence. Ensures that fun <| otherFun <cursor> yields the signature help of otherFun, not fun.

• 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 of fun, not otherFun.

• appArg : CandidateKind

  Cursor is in the position of the argument to a function that already has other arguments applied to it. High precedence.

def Lean.Server.FileWorker.SignatureHelp.CandidateKind.prio : CandidateKind → Nat

Equations

• Lean.Server.FileWorker.SignatureHelp.CandidateKind.pipeArg.prio = 0
• Lean.Server.FileWorker.SignatureHelp.CandidateKind.termArg.prio = 1
• Lean.Server.FileWorker.SignatureHelp.CandidateKind.appArg.prio = 2

structure Lean.Server.FileWorker.SignatureHelp.Candidate : Type

• kind : CandidateKind
• appStx : Syntax

inductive Lean.Server.FileWorker.SignatureHelp.SearchControl : Type

• 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.

def Lean.Server.FileWorker.SignatureHelp.findSignatureHelp? (text : FileMap) (ctx? : Option Lsp.SignatureHelpContext) (cmdStx : Syntax) (tree : Elab.InfoTree) (requestedPos : String.Pos.Raw) : IO (Option Lsp.SignatureHelp)

Equations

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