lean_completions
Retrieve IDE-style autocomplete suggestions for Lean code at a specified position. Provide file path, line, and column to get completions for incomplete expressions.
Instructions
Get IDE autocompletions. Use on INCOMPLETE code (after . or partial name).
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| line | Yes | Line number (1-indexed) | |
| column | Yes | Column number (1-indexed characters) | |
| file_path | Yes | Absolute or project-root-relative path to Lean file | |
| max_completions | No | Max completions | |
| resolve_details | No | Fetch type signatures for the top N results |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| items | No | List of completion items |