lean_multi_attempt
Try multiple Lean tactics without editing your file. Returns the goal state for each so you can compare and pick the right one.
Instructions
Try multiple tactics without modifying file. Returns goal state for each.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| line | Yes | Line number (1-indexed) | |
| column | No | Column (1-indexed). Omit to target the tactic line | |
| snippets | Yes | Tactics to try (3+ recommended) | |
| file_path | Yes | Absolute or project-root-relative path to Lean file |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| items | No | List of attempt results |