LSP: Function Parameter tips would be nice

[lovettchris]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

It is helpful in other languages to see highlighted help as you enter parameters to a function call.

Would be nice to get this on Lean also.

Steps to Reproduce

1. Type Array. and select append

Expected behavior: [What you expect to happen]

Get nice help on the fact that it expects 2 parameters, the first one is type Array and has the name "as" when you complete that one it highlights the second parameter, also type Array with the name "bs".

Actual behavior:

Good luck, there's no help on the parameters to this method once you've entered "append"

Reproduces how often: [What percentage of the time does it reproduce?] 100%

Versions

You can get this information from copy and pasting the output of lean --version, please include the OS and what version of the OS you're running.

Lean (version 4.0.0-nightly-2021-11-17, commit 25ebc68b875f, Release)

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.