lean_local_search
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) |