lean_goal
Read-onlyIdempotent
Retrieve proof goals at specific positions in Lean files to analyze tactic transformations and verify proof completion.
Instructions
Get proof goals at a position. MOST IMPORTANT tool - use often!
Omit column to see goals_before (line start) and goals_after (line end),
showing how the tactic transforms the state. "no goals" = proof complete.Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | Absolute path to Lean file | |
| line | Yes | Line number (1-indexed) | |
| column | No | Column (1-indexed). Omit for before/after |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| goals | No | Goal list at specified column position | |
| goals_after | No | Goals at line end (when column omitted) | |
| goals_before | No | Goals at line start (when column omitted) | |
| line_context | Yes | Source line where goals were queried |