lean_goal
Retrieve proof goals at a specific line in a Lean file to understand the current proof state and its evolution.
Instructions
Get the proof goals (proof state) at a specific location in a Lean file.
VERY USEFUL! Main tool to understand the proof state and its evolution!
Returns "no goals" if solved.
To see the goal at sorry, use the cursor before the "s".
Avoid giving a column if unsure-default behavior works well.
Args:
file_path (str): Abs path to Lean file
line (int): Line number (1-indexed)
column (int, optional): Column number (1-indexed). Defaults to None => Both before and after the line.
Returns:
str: Goal(s) or error msg
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| line | Yes | ||
| column | No | ||
| file_path | Yes |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |