lean_hover_info
Read-onlyIdempotent
Retrieve type signatures and documentation for symbols in Lean files to understand API functionality during theorem proving.
Instructions
Get type signature and docs for a symbol. Essential for understanding APIs.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | Absolute path to Lean file | |
| line | Yes | Line number (1-indexed) | |
| column | Yes | Column at START of identifier |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| info | Yes | Type signature and documentation | |
| symbol | Yes | The symbol being hovered | |
| diagnostics | No | Diagnostics at this position |