The Agda User Manual is a work-in-progress and is still incomplete. Contributions, additions and corrections to the Agda manual are greatly appreciated. To do so, please open a pull request or issue on the GitHub Agda page.

This is the manual for the Agda programming language, its type checking, compilation and editing system and related resources/tools.

You can find a lot of useful resources on Agda Wiki site, like tutorials, introductions, publications and books. If you’re new to Agda, you should make use of the resources on Agda Wiki and chapter Getting Started instead of chapter Language Reference.

A description of the Agda language is given in chapter Language Reference. Guidance on how the Agda editing and compilation system can be used can be found in chapter Tools.