lean_completions
Request IDE-style autocompletions for incomplete Lean code at a specific file position. Provide the file path, line, and column to get candidate names and type signatures, helping you finish expressions and discover available symbols.
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 |