lean_completions
Get IDE autocompletions for Lean theorem prover code by analyzing incomplete syntax after dots or partial names to suggest completions.
Instructions
Get IDE autocompletions. Use on INCOMPLETE code (after . or partial name).
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | Absolute path to Lean file | |
| line | Yes | Line number (1-indexed) | |
| column | Yes | Column number (1-indexed) | |
| max_completions | No | Max completions |