lean_completions
Get code completions for incomplete Lean code after a dot or partial name. Specify file path, line, and column to receive suggestions with optional type signatures.
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 |