Skip to main content
Glama
Sign In
Lean LSP MCP

Lean LSP MCP

by oOo0oOo
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Hybrid

lean_declaration_file

Read-onlyIdempotent

Retrieve Lean declaration source by file path and symbol, including its line range and configurable surrounding context; optionally return the entire file.

Instructions

Get declaration source with the source-line range and surrounding context.

Generated declarations include their source declaration when it is clear.
Set full_file=True for the whole file (can be very large).

Input Schema

NameRequiredDescriptionDefault
symbolYesCase-sensitive Lean name in the file or project environment
file_pathYesAbsolute or project-root-relative path to Lean file
full_fileNoReturn the entire declaration file (large!)
context_linesNoLines of context around the declaration

Output Schema

NameRequiredDescriptionDefault
contentYesDeclaration source (sliced unless full_file=True)
end_lineNoLast line of the returned slice (1-indexed)
file_pathYesPath to declaration file
start_lineNoFirst line of the returned slice (1-indexed)
total_linesNoTotal lines in the declaration file
source_declarationNoSource declaration for a generated declaration such as one created by @[to_additive], when it can be determined reliably
declaration_end_lineNoDeclaration end line (1-indexed), when known
declaration_start_lineNoDeclaration start line (1-indexed)

Schema Changelog

Changes observed during successful MCP inspections.

  1. Changed4 schema fields changedv0.33.0
    • changedInput schema / properties / symbol / description
      Previous value: -"Symbol (case sensitive, must be in file)"New value: +"Case-sensitive Lean name in the file or project environment"
    • addedOutput schema / properties / declaration_end_line
      Added value: +{
+  "anyOf": [
+    {
+      "type": "integer"
+    },
+    {
+      "type": "null"
+    }
+  ],
+  "default": null,
+  "description": "Declaration end line (1-indexed), when known",
+  "title": "Declaration End Line"
+}
    • addedOutput schema / properties / declaration_start_line
      Added value: +{
+  "anyOf": [
+    {
+      "type": "integer"
+    },
+    {
+      "type": "null"
+    }
+  ],
+  "default": null,
+  "description": "Declaration start line (1-indexed)",
+  "title": "Declaration Start Line"
+}
    • addedOutput schema / properties / source_declaration
      Added value: +{
+  "anyOf": [
+    {
+      "type": "string"
+    },
+    {
+      "type": "null"
+    }
+  ],
+  "default": null,
+  "description": "Source declaration for a generated declaration such as one created by @[to_additive], when it can be determined reliably",
+  "title": "Source Declaration"
+}
  2. Changed6 schema fields changedv0.28.0
    • addedInput schema / properties / context_lines
      Added value: +{
+  "default": 20,
+  "description": "Lines of context around the declaration",
+  "minimum": 0,
+  "title": "Context Lines",
+  "type": "integer"
+}
    • addedInput schema / properties / full_file
      Added value: +{
+  "default": false,
+  "description": "Return the entire declaration file (large!)",
+  "title": "Full File",
+  "type": "boolean"
+}
    • changedOutput schema / properties / content / description
      Previous value: -"File content"New value: +"Declaration source (sliced unless full_file=True)"
    • addedOutput schema / properties / end_line
      Added value: +{
+  "anyOf": [
+    {
+      "type": "integer"
+    },
+    {
+      "type": "null"
+    }
+  ],
+  "default": null,
+  "description": "Last line of the returned slice (1-indexed)",
+  "title": "End Line"
+}
    • addedOutput schema / properties / start_line
      Added value: +{
+  "anyOf": [
+    {
+      "type": "integer"
+    },
+    {
+      "type": "null"
+    }
+  ],
+  "default": null,
+  "description": "First line of the returned slice (1-indexed)",
+  "title": "Start Line"
+}
    • addedOutput schema / properties / total_lines
      Added value: +{
+  "anyOf": [
+    {
+      "type": "integer"
+    },
+    {
+      "type": "null"
+    }
+  ],
+  "default": null,
+  "description": "Total lines in the declaration file",
+  "title": "Total Lines"
+}
  3. Addedv0.10.0
  4. Removedv0.23.1
  5. First observed

TDQS

A3.8/5.0
Behavior4/5

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

Annotations already establish this as a readOnly, idempotent, closed-world lookup, so the description only needs to add behavior beyond that. It does add two useful facts: generated declarations conditionally include their source declaration, and full_file can return a very large payload. It does not say what happens when the symbol is missing or not found in the given file, which is the main remaining gap.

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?

Three short sentences, each carrying a distinct point (what is returned, generated-declaration behavior, the large-file escape hatch), with the core purpose front-loaded. Nothing is wasted or restated from the title.

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?

An output schema exists, so return-shape explanation is properly omitted, and for a simple read tool the description covers purpose, one behavioral nuance, and a size caveat. The only meaningful omission is how this differs from adjacent lookup siblings, which would help an agent pick correctly in a crowded toolset.

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

Parameters3/5

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

Schema description coverage is 100%, so symbol, file_path, full_file, and context_lines are already documented in structured form and the baseline is 3. The description slightly reinforces full_file with a size warning and implicitly links context_lines to 'surrounding context', but adds no format or edge-case meaning beyond the schema.

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

Purpose4/5

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

States a concrete verb and resource: retrieve a declaration's source along with its source-line range and surrounding context. That is far more specific than the title alone and distinguishes it from listing tools like lean_file_outline. It stops short of naming a sibling such as lean_hover_info, so the differentiation from related lookup tools is left implicit.

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

Usage Guidelines3/5

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

Usage is implied by the stated output (declaration source with line range), but there is no explicit when-to-use versus lean_hover_info, lean_file_outline, or lean_local_search, and no stated preconditions beyond the schema's path/symbol requirements. The one behavioral caveat given is the full_file escape hatch, which guides usage but is not an alternative-selection rule.

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

Deploy Server

Other Tools