lean_multi_attempt
Try multiple tactics at a specific line in a Lean file without modifying it. Returns goal states for each tactic attempt.
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 |