Skip to main content
Glama
DreamLinuxer

agda-mcp

by DreamLinuxer
OverviewSchemaRelated ServersScoreDiscussions
Python
Local

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.

Related MCP server: lean-lsp-mcp

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.

Install Server
F
license - not found
B
quality
D
maintenance

How are these scores calculated?

Maintenance

–Maintainers
–Response time
–Release cycle
–Releases (12mo)
Commit activity

Resources

Unclaimed servers have limited discoverability.

Looking for Admin?

If you are the server author, to access and configure the admin panel.

Tools

View all tools

Related MCP Servers

View all related MCP servers

Related MCP Connectors

  • mcp

    Augments MCP Server - A comprehensive framework documentation provider for Claude Code

  • Remote Desktop Commander

    Hosted MCP server connecting claude.ai, ChatGPT and other AI apps to your own computer

  • microservices.sh

    MCP server for AI agents to plan, verify, and deploy Cloudflare-native apps.

View all MCP Connectors

Latest Blog Posts

MCP directory API

We provide all the information about MCP servers via our MCP API.

curl -X GET 'https://glama.ai/api/mcp/v1/servers/DreamLinuxer/agda-mcp'

If you have feedback or need assistance with the MCP directory API, please join our Discord server