lean_completions
Get Lean code completions at a file location, including dot completions, identifier suggestions, and importable file lists after 'import'. Use on incomplete lines to discover available identifiers and imports.
Instructions
Get code completions at a location in a Lean file.
Only use this on INCOMPLETE lines/statements to check available identifiers and imports:
- Dot Completion: Displays relevant identifiers after a dot (e.g., `Nat.`, `x.`, or `Nat.ad`).
- Identifier Completion: Suggests matching identifiers after part of a name.
- Import Completion: Lists importable files after `import` at the beginning of a file.
Args:
file_path (str): Abs path to Lean file
line (int): Line number (1-indexed)
column (int): Column number (1-indexed)
max_completions (int, optional): Maximum number of completions to return. Defaults to 32
Returns:
str: List of possible completions or error msg
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| line | Yes | ||
| column | Yes | ||
| file_path | Yes | ||
| max_completions | No |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |