lean_code_actions
Retrieve code actions for a specific line in a Lean file, including TryThis suggestions (simp?, exact?, apply?) and quick fixes, with resolved edits.
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 |