lean_local_search
Read-onlyIdempotent
Verify Lean theorem prover declarations exist locally before using them. Search project files to confirm lemma names and avoid errors.
Instructions
Fast local search to verify declarations exist. Use BEFORE trying a lemma name.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| query | Yes | Declaration name or prefix | |
| limit | No | Max matches | |
| project_root | No | Project root (inferred if omitted) |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| items | No | List of local search results |