lean_code_actions
Resolve code actions and quick fixes for a specified line in a Lean file, returning resolved edits for suggestions like TryThis, exact, apply, and other LSP actions.
Instructions
Get LSP code actions for a line. Returns resolved edits for TryThis suggestions (simp?, exact?, apply?) and other quick fixes.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| line | Yes | Line number (1-indexed) | |
| file_path | Yes | Absolute path to Lean file |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| actions | No | List of available code actions |