lean_hover_info

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations already declare readOnlyHint=true and idempotentHint=true, so the description does not need to repeat those. It adds the behavioral insight that the tool returns type signatures and documentation, which is useful context beyond annotations. No contradictions.

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?

The description is a single sentence that conveys the tool's purpose efficiently. No unnecessary words or redundancy. It is well-structured and front-loaded.

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?

Given that an output schema exists (not shown but present), the description does not need to explain return values. The description covers the core purpose and context. However, it could mention that the file must be opened in the Lean environment, but that is implicitly understood from the tool's nature.

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 description coverage is 100%, with each parameter having a clear description. The tool description does not add any additional parameter information, so a baseline score of 3 is appropriate.

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?

The description clearly states 'Get type signature and docs for a symbol', which is a specific verb+resource pair. It distinguishes from sibling tools like lean_completions or lean_goal by focusing on type information and documentation.

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 phrase 'Essential for understanding APIs' implies when to use it, but there is no explicit guidance on when not to use it or how it compares to alternatives like lean_declaration_file or lean_references. Usage context is implied but not fully elaborated.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.