Agda-mcp brings the full power of Agda's interactive development environment to any MCP client, including Claude Code. By leveraging the `agda --interaction-json` interface, the server provides essential features like type checking, go-to-definition, case splitting, and automated proof search, without the need for an additional language server. It seamlessly integrates Agda's sophisticated capabilities into your development workflow, enhancing productivity and enabling deeper interaction with your formal proofs and programs.
Key Features
01Type inference and expression evaluation
02Case splitting on variables in goals
030 GitHub stars
04Type checking and diagnostics for Agda files
05Go-to-definition for symbols
06Automated proof search for goals
