Agda

A dependently typed functional programming language and proof assistant

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

Version on this page:2.6.2.2@rev:2
LTS Haskell 22.43:2.6.4.3@rev:1
Stackage Nightly 2024-12-09:2.7.0.1@rev:2
Latest on Hackage:2.7.0.1@rev:2

See all snapshots Agda appears in

LicenseRef-OtherLicense licensed by Ulf Norell and 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.2.2@sha256:b69c2f317db2886cb387134af00a3e42a06fab6422686938797924d034255a55,37047

Module documentation for 2.6.2.2

Agda 2

Hackage version Stackage version Test Stack Build Status via GH Actions 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.

Documentation

Getting Started

Contributing to Agda

Changes

Release notes for Agda version 2.6.2.2

Highlights

  • Agda 2.6.2.2 catches up to changes in the Haskell ecosystem (bytestring-0.11.2.0, mtl-2.3-rc3/4, text-icu-0.8.0.1, stackage lts-19.0 and nightly).

  • Fixes inconsistency #5838 in --cubical.

  • Fixes some regressions introduced in 2.6.1:

    • #5809: internal error with --irrelevant-projections.
  • Fixes some regressions introduced in 2.6.2:

    • #5705 and #5706: inconsistency from universe level Int overflow.

    • #5784: primEraseEquality does not compute.

    • #5805: internal error involving holes and with.

    • #5819: internal error when reducing in termination checker.

  • Other fixes and improvements (see below).

Installation and infrastructure

Agda supports GHC versions 8.0.2 to 9.2.2.

  • UTF-8 encoding is now used for the libraries and executables configuration files (issue #5741).

Language

  • macro definitions can now be used even when they are declared as erased (PR #5744). For example, this is now accepted:

    macro
      @0 trivial : Term → TC ⊤
      trivial = unify (con (quote refl) [])
    
    test : 42 ≡ 42
    test = trivial
    
  • Fixed inconsistent --cubical reductions for transp: issue #5838.

  • Fixed issues with reflection:

    • #5762: do not eagerly check existence of commands in executables file.

    • #5695: fix elaborate-and-give interaction command.

    • #5700: scope of metas created during macro expansion.

    • #5712: internal error with tactics on record fields of function type.

  • Fixed issues with instance search:

    • #5583: constructor instances from parameterized modules.

    • #5787: erased instance arguments.

  • Fixed issue #5683 with generalization in let.

Compiler backends

  • .hs files generated by the GHC backend now switch off the warn-overlapping-patterns warning (issue #5758).

  • The GHC backend now calls ghc with environment setting GHC_CHARENC=UTF-8 (issue #5742).

Performance

  • Better caching of interfaces (issue #2767).

  • Various performance improvements concerning meta-variables: issue #5388 and PR #5733.