textDocument/signatureHelp

Stream: lean4

[Julian Berman]

Do there happen to be any thoughts of implementing signature help support in the server such that one sees just the arguments which are not implicit when constructing a term? I.e. show any argument that needs providing in the signature help, as opposed to the hover which often shows some ungodly long list.

[Marc Huisinga]

This is lean4#806, by the way. It will be implemented eventually as the language server becomes more feature complete.

[Mauricio Collares]

(deleted)