agda-mcp
Server Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||
Instructions
Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.
This server publishes no instructions, or was last inspected before Glama recorded them.
Capabilities
Features and capabilities supported by this server
Protocol revision2025-11-25
| Capability | Details |
|---|---|
| tools | {
"listChanged": false
} |
| prompts | {
"listChanged": false
} |
| resources | {
"subscribe": false,
"listChanged": false
} |
| experimental | {} |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| agda_loadA | Load and type-check an Agda file. Returns goals, errors, and warnings. This must be called before other commands. Call again after edits to refresh. Args: file_path: Absolute path to the .agda file |
| agda_hoverA | Get type/definition info for a symbol at a position. Args: file_path: Absolute path to the .agda file line: Line number (1-based) character: Column number (1-based) |
| agda_definitionB | Go to the definition of a symbol at a position. Args: file_path: Absolute path to the .agda file line: Line number (1-based) character: Column number (1-based) |
| agda_inferA | Infer the type of an expression in the context of a loaded file. Args: file_path: Absolute path to the .agda file (for scope) expr: The expression to type-check (e.g. "add", "suc zero") |
| agda_computeA | Normalize (evaluate) an expression. Args: file_path: Absolute path to the .agda file (for scope) expr: The expression to evaluate (e.g. "add 2 3") |
| agda_case_splitA | Case split on a variable in a goal. Returns the new clauses. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) variable: The variable name to split on |
| agda_goal_infoA | Get the type and context of a specific goal/hole. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) |
| agda_autoB | Try to automatically solve a goal. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) |
| agda_why_in_scopeA | Explain where a name is brought into scope. Args: file_path: Absolute path to the .agda file name: The name to look up (e.g. "ℕ", "suc", "add") |
| agda_giveA | Fill a goal/hole with a complete solution. Agda will check the expression and, if correct, replace the hole in the source file. Call agda_load afterwards to refresh goals. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: The expression to fill the hole with |
| agda_elaborate_giveA | Fill a goal/hole with an elaborated solution. Like agda_give, but returns the fully elaborated (normalized) expression. Call agda_load afterwards to refresh goals. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: The expression to fill the hole with |
| agda_refineA | Refine a goal by filling it with an expression that may create new subgoals. If expr is empty, Agda tries to refine using the goal type. Call agda_load afterwards to refresh goals. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: Expression to refine with (can be empty) |
| agda_introA | Introduce a constructor or lambda abstraction in a goal. Tries to fill the hole with an appropriate constructor or lambda. Call agda_load afterwards to refresh goals. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) |
| agda_refine_or_introA | Refine or introduce in a goal (auto-chooses the best action). Combines refine and intro: tries to refine with the expression if given, otherwise introduces a constructor or lambda. Call agda_load afterwards to refresh goals. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: Expression to refine with (can be empty for intro) |
| agda_goal_typeA | Get the type of a specific goal/hole (without context). Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) |
| agda_contextA | Get the context (available bindings) at a specific goal/hole. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) |
| agda_goal_type_context_inferB | Get goal type, context, and the inferred type of an expression. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: Expression whose type to infer in this goal's context |
| agda_goal_type_context_checkB | Get goal type, context, and check an expression against the goal type. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: Expression to check against the goal type |
| agda_infer_in_goalA | Infer the type of an expression in the context of a specific goal. Unlike agda_infer which works at top level, this infers within a goal's local context (with access to locally-bound variables). Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: The expression to type-check |
| agda_compute_in_goalA | Normalize (evaluate) an expression in the context of a specific goal. Unlike agda_compute which works at top level, this evaluates within a goal's local context. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: The expression to evaluate |
| agda_helper_functionA | Generate a helper function type signature for a goal. The expression should be a partial application like "h x y" where h is the helper name and x, y are arguments. Agda will generate the type signature for h. If empty, uses whatever is in the goal. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: Partial application (e.g. "helper x y") |
| agda_why_in_scope_goalA | Explain where a name is brought into scope, in the context of a goal. Like agda_why_in_scope but with access to the goal's local scope. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) name: The name to look up |
| agda_module_contents_goalA | List the contents of a module, in the context of a goal. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) module_name: The module or record name to inspect |
| agda_solve_oneA | Solve a single goal if its solution has been determined by unification. Only works if the goal has been fully instantiated (e.g. by constraints). Call agda_load afterwards to refresh goals. Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) |
| agda_solve_allA | Solve all goals whose solutions have been determined by unification. Call agda_load afterwards to refresh goals. Args: file_path: Absolute path to the .agda file |
| agda_auto_allA | Try to automatically solve all visible goals. Call agda_load afterwards to refresh goals. Args: file_path: Absolute path to the .agda file |
| agda_constraintsA | Show all current unsolved constraints. Useful for debugging type errors or understanding what Agda is stuck on. Args: file_path: Absolute path to the .agda file |
| agda_metasA | Show all open meta-variables (goals) and their types. Args: file_path: Absolute path to the .agda file |
| agda_search_aboutA | Search for definitions whose type mentions the given names. Useful for finding relevant lemmas, functions, or constructors. Args: file_path: Absolute path to the .agda file query: Space-separated names to search for in types |
| agda_module_contentsB | List the top-level names exported by a module. Args: file_path: Absolute path to the .agda file module_name: The module name to inspect (e.g. "Data.Nat", "Data.List") |
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
No resources | |
TDQS
Scored across 30 tools
Many tools overlap significantly, especially the goal-info variants (agda_goal_info, agda_goal_type, agda_context, agda_goal_type_context_infer, agda_goal_type_context_check) and the top-level vs goal-local pairs (agda_infer vs agda_infer_in_goal, agda_compute vs agda_compute_in_goal, agda_why_in_scope vs agda_why_in_scope_goal). Agents will struggle to choose the correct tool among these near-duplicates.
All tools use the 'agda_' prefix and lowercase snake_case, with a mostly verb_noun structure (load, case_split, infer, compute, give, refine, intro, solve). A few names deviate (e.g., agda_definition, agda_goal_type_context_infer) but the overall pattern is predictable and consistent.
With 30 tools, the server exceeds the 25-tool threshold considered heavy. While the domain of Agda interaction is broad, many tools are redundant variants (e.g., agda_solve_one vs agda_solve_all, agda_auto vs agda_auto_all), suggesting the count could be trimmed without losing functionality.
The tool set covers the core Agda workflow well: loading files, inspecting goals, case splitting, giving/refining/intro, automatic solving, constraint/meta inspection, and module exploration. Minor gaps exist (e.g., no explicit 'revert' or 'abort' command), but agents can work around these with existing tools.