lean_state_search
Read-onlyIdempotent
Find relevant lemmas to close proof goals in Lean files by searching premise-search.com based on specific file positions.
Instructions
Limit: 3req/30s. Find lemmas to close the goal at a position. Searches premise-search.com.
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) | |
| num_results | No | Max results |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| items | No | List of state search results |