Agda

A dependently typed functional programming language and proof assistant

https://wiki.portal.chalmers.se/agda/

Version on this page:	2.6.4.3@rev:1
LTS Haskell 22.40:	2.6.4.3@rev:1
Stackage Nightly 2024-11-08:	2.7.0.1@rev:2
Latest on Hackage:	2.7.0.1@rev:2

See all snapshots Agda appears in

MIT licensed by The Agda Team, see https://agda.readthedocs.io/en/latest/team.html

Maintained by The Agda Team

This version can be pinned in stack with:Agda-2.6.4.3@sha256:a8066d4b15827534d118846e98fd47bb9aadeb75e3d3b1f2c3bda8f5885c3f7c,29246

Module documentation for 2.6.4.3

Agda

Depends on 45 packages(full list with versions):

aeson, Agda, ansi-terminal, array, async, base, binary, blaze-html, boxes, bytestring, case-insensitive, containers, data-hash, deepseq, directory, dlist, edit-distance, equivalence, exceptions, filepath, ghc-compact, gitrev, hashable, haskeline, monad-control, mtl, murmur-hash, parallel, peano, pretty, process, regex-tdfa, split, stm, STMonadTrans, strict, text, time, time-compat, transformers, and many more

Used by 1 package in lts-22.40(full list with versions):

Agda 2

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.

Documentation

User manual (per-commit pdf can be downloaded from the github actions page)
CHANGELOG

Getting Started

Contributing to Agda

Contribution how-to: HACKING
Haskell style-guide

Changes

Release notes for Agda version 2.6.4.3

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

Agda 2.6.4.3 supports GHC versions 8.6.5 to 9.8.1.

Closed issues

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

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