Find Lean 4 declaration definitions and navigate to them instantly without network latency, using pre-built .ilean caches for offline lookup.
Offline zero-latency symbol lookup and jump-to-definition via pre-compiled .ilean cache
| Name | Required | Description | Default |
|---|---|---|---|
| symbol | Yes | Lean declaration name (e.g. RealQ.bellmanOp or BoundedRewardKernel) | |
| preferOfflineIlean | No | Use fast .ilean cache (default true) |
Changes observed during successful MCP inspections.
v0.1.0Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the behavioral burden. It discloses that the tool operates offline, uses a pre-compiled .ilean cache, and is optimized for zero-latency lookups, which are meaningful beyond the schema. It stops short of stating whether cache writes or refresh operations can occur, but for a lookup operation the read-only intent is reasonably clear.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single well-formed sentence that front-loads the primary action and then specifies the mechanism. There is no redundancy or filler.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a two-parameter lookup tool with full schema descriptions, the description plus schema is largely sufficient for an agent to select and invoke it. It does not describe the return payload or cache-miss behavior, but the core selection and invocation context is present.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 100%, so the parameter meanings are already fully documented. The description adds no additional semantics beyond reinforcing the cache behavior already reflected in preferOfflineIlean.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States a specific verb and resource: symbol lookup and jump-to-definition, with the exact mechanism (.ilean cache). This is clearly distinct from sibling tools focused on goals, module hierarchy, or FFI inspection.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The intent is implied: use this when you need a fast offline symbol lookup or jump-to-definition. It does not explicitly state when to prefer or avoid sibling tools, so no exclusion guidance is provided.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.