lean_declaration_file
Read-onlyIdempotent
Locate where a symbol is declared in a Lean file to understand its definition and usage context.
Instructions
Get file where a symbol is declared. Symbol must be present in file first.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | Absolute path to Lean file | |
| symbol | Yes | Symbol (case sensitive, must be in file) |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| content | Yes | File content | |
| file_path | Yes | Path to declaration file |