- eager : Lean.Lsp.CodeAction
This is the initial code action that is sent to the server, to implement
A code action optionally supporting a lazy code action computation that is only run when the user clicks on the code action in the editor.
If you want to use the lazy feature, make sure that the
edit? field on the
eager code action result is
- params : Lean.Lsp.CodeActionParams
- providerName : Lake.Name
Name of CodeActionProvider that produced this request.
- providerResultIndex : Nat
Index in the list of code action that the given provider generated.
Passed as the
data? field of
Lsp.CodeAction to recover the context of the code action.
A code action provider is a function for providing LSP code actions for an editor.
You can register them with the
This is a low-level interface for making LSP code actions. This interface can be used to implement the following applications:
- refactoring code: adding underscores to unused variables,
- suggesting imports
- document-level refactoring: removing unused imports, sorting imports, formatting.
- Helper suggestions for working with type holes (
- Helper suggestions for tactics.
When implementing your own
CodeActionProvider, we assume that no long-running computations are allowed.
If you need to create a code-action with a long-running computation, you can use the
lazy? field on
to perform the computation after the user has clicked on the code action in their editor.