A dependently typed functional programming language and proof assistant

Version on this page:
LTS Haskell 22.30:
Stackage Nightly 2024-07-24:
Latest on Hackage:

See all snapshots Agda appears in

MIT licensed by The Agda Team, see
Maintained by The Agda Team
This version can be pinned in stack with:Agda-,29214

Module documentation for

Agda 2

Hackage version Stackage version Test Documentation Status Agda Zulip

The official Agda logo

Note that this README is only about Agda, not its standard library. See the Agda Wiki for information about the library.


Getting Started

Contributing to Agda


Release notes for Agda version

This release fixes a regression in and one in 2.6.4. It aims to be API-compatible with and

Agda supports GHC versions 8.6.5 to 9.8.1.

Closed issues

For, the following issues were closed (see bug tracker):

  • Issue #7148: Regression in concerning with
  • Issue #7150: Regression in 2.6.4 in rewrite with instances