lean_references
Find every reference to a symbol in a Lean project, including its declaration, by specifying the file path, line, and column where the symbol appears.
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 | |
| max_results | No | Max locations to return (default 50) |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| items | No | List of reference locations | |
| total | No | Total matches (> len(items) when truncated by max_results) |