lean_multi_attempt
Test multiple Lean code snippets at a line to compare tactics and approaches. Returns goal states and diagnostics for each alternative.
Instructions
Try multiple Lean code snippets at a line and get the goal state and diagnostics for each.
Use to compare tactics or approaches.
Use rarely-prefer direct file edits to keep users involved.
For a single snippet, edit the file and run `lean_diagnostic_messages` instead.
Note:
Only single-line, fully-indented snippets are supported.
Avoid comments for best results.
Args:
file_path (str): Abs path to Lean file
line (int): Line number (1-indexed)
snippets (List[str]): List of snippets (3+ are recommended)
Returns:
List[str] | str: Diagnostics and goal states or error msg
Tool call template
Replace each placeholder with a value matching the input schema. Only required parameters are included; add optional parameters as needed.
{
"id": 1,
"jsonrpc": "2.0",
"method": "tools/call",
"params": {
"arguments": {
"file_path": "<file_path>",
"line": "<line>",
"snippets": "<snippets>"
},
"name": "lean_multi_attempt"
}
}Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| line | Yes | ||
| snippets | Yes | ||
| file_path | Yes |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |