lean_file_outline
Read-onlyIdempotent
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 |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| imports | No | Import statements | |
| declarations | No | Top-level declarations |