agda-mcp

agda-mcp

MCP server for Agda, providing type checking, go-to-definition, case splitting, auto proof search, and more — directly from Claude Code or any MCP client.

Talks to agda --interaction-json (the same interface powering agda-mode in Emacs/VS Code), so it has access to all of Agda's interactive features without needing agda-language-server.

Installation

Prerequisites

• Agda (tested with 2.8.0) — agda must be on your PATH
• uv

1. Clone and build

git clone https://github.com/DreamLinuxer/agda-mcp.git
cd agda-mcp
uv sync

2. Add to your MCP client

Claude Code (globally, for all projects):

claude mcp add --scope user agda-lsp -- uv run --directory /path/to/agda-mcp agda-mcp

Other MCP clients — add to your client's MCP config:

{
  "mcpServers": {
    "agda-lsp": {
      "command": "uv",
      "args": ["run", "--directory", "/path/to/agda-mcp", "agda-mcp"],
      "type": "stdio"
    }
  }
}

Replace /path/to/agda-mcp with the absolute path where you cloned the repo.

Tools

File & navigation

| Tool | Description | |------|-------------| | agda_load | Load/type-check a file, get goals + errors + warnings | | agda_hover | Symbol kind + definition site at a position | | agda_definition | Go to definition (file:line:col) |

Goal manipulation (modify source)

| Tool | Description | |------|-------------| | agda_give | Fill a hole with a complete solution | | agda_elaborate_give | Fill a hole with an elaborated solution | | agda_refine | Refine a goal (may create new subgoals) | | agda_intro | Introduce a constructor or lambda | | agda_refine_or_intro | Auto-choose between refine and intro | | agda_case_split | Case split on a variable in a goal | | agda_auto | Try to automatically solve a goal | | agda_solve_one | Solve a goal if determined by unification |

Goal inspection

| Tool | Description | |------|-------------| | agda_goal_info | Get the type and context of a goal | | agda_goal_type | Get just the type of a goal | | agda_context | Get the context (bindings) at a goal | | agda_goal_type_context_infer | Goal type + context + inferred type of expr | | agda_goal_type_context_check | Goal type + context + check expr against type | | agda_infer_in_goal | Infer type of an expression at a goal | | agda_compute_in_goal | Normalize an expression at a goal | | agda_helper_function | Generate helper function type for a goal | | agda_why_in_scope_goal | Explain where a name comes from (at a goal) | | agda_module_contents_goal | List module contents (at a goal) |

Toplevel commands

| Tool | Description | |------|-------------| | agda_infer | Infer the type of an expression | | agda_compute | Normalize/evaluate an expression | | agda_why_in_scope | Explain where a name comes from | | agda_constraints | Show all unsolved constraints | | agda_metas | Show all open goals/meta-variables | | agda_search_about | Search for definitions mentioning given names | | agda_module_contents | List names exported by a module | | agda_solve_all | Solve all goals determined by unification | | agda_auto_all | Try to automatically solve all goals |

Usage examples

Load and type-check a file

agda_load("/path/to/file.agda")
→ Checked. No errors, warnings, or goals.

Infer a type

agda_infer("/path/to/file.agda", "map")
→ {a b : Set} {n : ℕ} → (a → b) → Vec a n → Vec b n

Evaluate an expression

agda_compute("/path/to/file.agda", "2 + 3")
→ 5

Case split

agda_case_split("/path/to/file.agda", 0, "xs")
→ f [] = ?
  f (x ∷ xs) = ?

Auto-solve a goal

agda_auto("/path/to/file.agda", 0)
→ a , b

How it works

The server spawns a single persistent agda --interaction-json process and communicates via the IOTCM protocol over stdio. File state (highlighting data for go-to-definition, goal types, diagnostics) is cached per file and refreshed on each agda_load call.