lean_declaration_file
Locate the declaration file for a specific symbol in Lean code 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) |