lean_references
Retrieve all references to a symbol, including its declaration, by specifying the file path, line, and column position.
Instructions
Find all references to a symbol (including the declaration). Position cursor at the symbol.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| line | Yes | Line number (1-indexed) | |
| column | Yes | Column at START of identifier (1-indexed) | |
| file_path | Yes | Absolute path to Lean file |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| items | No | List of reference locations |