lean_term_goal
Retrieve the expected type or goal at a specified line and column in a Lean file to understand the type of an expression at that position.
Instructions
Get the expected type at a position.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| line | Yes | Line number (1-indexed) | |
| column | No | Column (defaults to end of line) | |
| file_path | Yes | Absolute or project-root-relative path to Lean file |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| line_context | Yes | Source line where term goal was queried | |
| expected_type | No | Expected type at this position |