lean_file_outline
Extract imports and declarations with type signatures from Lean files to understand code structure efficiently.
Instructions
Get imports and declarations with type signatures. Token-efficient.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | Absolute path to Lean file |