lean_completions
Get IDE autocompletions for Lean code by specifying the file path, line, and column. Use it on incomplete code after a dot or partial name to see completion suggestions.
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) | |
| file_path | Yes | Absolute or project-root-relative path to Lean file | |
| max_completions | No | Max completions |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| items | No | List of completion items |