lean_term_goal
Retrieve the expected type at a specific position in a Lean file to understand type requirements and guide proof development.
Instructions
Get the expected type at a position.
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 (defaults to end of line) |