lean_local_search
Check the current Lean workspace for existing declarations by prefix, returning their kind and file to prevent API hallucination.
Instructions
Confirm declarations exist in the current workspace to prevent hallucinating APIs.
VERY USEFUL AND FAST!
Pass a short prefix (e.g. ``map_mul``); the metadata shows the declaration kind and file.
The index spans theorems, lemmas, defs, classes, instances, structures, inductives, abbrevs, and opaque decls.
Args:
query (str): Declaration name or prefix.
limit (int): Max matches to return (default 10).
Returns:
List[Dict[str, str]] | str: Matches as ``{"name", "kind", "file"}`` or error message.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| limit | No | ||
| query | Yes | ||
| project_root | No |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |