lean-lsp-mcp

lean_hover_info

Retrieve documentation and type information for a term at a given line and column in a Lean file.

Instructions

Get hover info (docs for syntax, variables, functions, etc.) at a specific location in a Lean file.

Args:
    file_path (str): Abs path to Lean file
    line (int): Line number (1-indexed)
    column (int): Column number (1-indexed). Make sure to use the start or within the term, not the end.

Returns:
    str: Hover info or error msg

Tool call template

Replace each placeholder with a value matching the input schema. Only required parameters are included; add optional parameters as needed.

{
  "id": 1,
  "jsonrpc": "2.0",
  "method": "tools/call",
  "params": {
    "arguments": {
      "file_path": "<file_path>",
      "line": "<line>",
      "column": "<column>"
    },
    "name": "lean_hover_info"
  }
}

Input Schema

Name	Required	Description	Default
`line`	Yes
`column`	Yes
`file_path`	Yes

Output Schema

Name	Required	Description	Default
`result`	Yes

Schema Changelog

Changes observed during successful MCP inspections.

First observedv0.14.1Aug 2, 2026

TDQS

A4.5/5.0

Behavior4/5

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

No annotations are provided, so the description carries the burden. It discloses that the return is a string containing hover info or an error message, and it adds a behavioral nuance about column placement. It does not detail preconditions like file state, but for a read-only hover tool, this is reasonable.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is compact and well-organized with Args and Returns sections. Every sentence contributes new information, and there is no redundancy.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

For a simple hover tool, the description covers all necessary inputs, the return type, and a practical positional caveat. The output schema is minimal (just a string), so the description adequately explains the return. It lacks explicit comparison to other tools, but that is addressed in the guidance dimension.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters5/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The input schema has zero parameter descriptions, so the description fully compensates. It explains each parameter with type and meaning, and specifically adds valuable guidance on the column parameter to avoid pointing at the end of a term. This is essential for correct invocation.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description states 'Get hover info' with the resource being a specific location in a Lean file, and augments it with 'docs for syntax, variables, functions, etc.' This clearly distinguishes it from sibling tools like lean_goal or lean_completions.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description provides clear context: use it at a specific file location to obtain hover documentation. It also gives a practical guideline about column position (start or within the term, not the end). It does not explicitly name alternatives, but the intended use is obvious.

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