lean_multi_attempt
Test multiple Lean tactics simultaneously on a goal without editing the file, returning the goal state for each tactic.
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 |