lean_file_outline
Extract imports and declarations with type signatures from Lean files to analyze project structure efficiently.
Instructions
Get imports and declarations with type signatures. Token-efficient.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | Absolute or project-root-relative path to Lean file | |
| max_declarations | No | Max declarations to return |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| imports | No | Import statements | |
| declarations | No | Top-level declarations | |
| total_declarations | No | Total count (set when truncated) |