Agda: A dependently typed functional programming language and proof assistant

[ dependent-types, program ] [ Propose Tags ]

Agda is a dependently typed functional programming language: It has inductive families, which are similar to Haskell's GADTs, but they can be indexed by values and not just types. It also has parameterised modules, mixfix operators, Unicode characters, and an interactive Emacs interface (the type checker can assist in the development of your code).

Agda is also a proof assistant: It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It has many similarities with other proof assistants based on dependent types, such as Coq, Epigram and NuPRL.

Note that if you want to use the command-line program (agda), then you should also install the Agda-executable package. The Agda package includes an Emacs mode for Agda, but you need to set up the Emacs mode yourself (for instance by running agda-mode setup; see the README).

Note also that this library does not follow the package versioning policy, because the library is only intended to be used by the Emacs mode and the Agda-executable package.

[Skip to Readme]




Automatic Flags

Try to use the character encoding specified by the locale for most of the IO going to/from stdin and stdout. (Note that source files must always be encoded using UTF8.)


Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info


Versions [RSS] 2.2.0, 2.2.2, 2.2.4, 2.2.6, 2.2.8, 2.2.10, 2.3.0,, 2.3.2,,, 2.4.0,,, 2.4.2,,,,,, 2.5.1,,, 2.5.2, 2.5.3, 2.5.4,,, 2.6.0,, 2.6.1,,,, 2.6.2,,, 2.6.3 (info)
Dependencies array (>=0.1 && <1), base (>=4.1 && <4.3), binary (>=0.4.4 && <0.6), bytestring (>= && <1), containers (>=0.1.0 && <1), directory (>=1 && <2), filepath (>=1.1 && <2), haskeline (>=0.3 && <0.7), haskell-src (>= && <2), mtl (>=1.1 && <2), old-time (>=1 && <2), pretty (>=1 && <2), process (>= && <2), QuickCheck (>= && <2.2), syb (>=0.1 && <0.2), utf8-string (>=0.3 && <0.4), xhtml (>=3000.2 && <3000.3), zlib (>= && <1) [details]
License LicenseRef-OtherLicense
Author Ulf Norell, Nils Anders Danielsson, Catarina Coquand, Makoto Takeyama, Andreas Abel, ...
Maintainer Ulf Norell <>
Category Dependent types
Home page
Bug tracker
Source repo head: darcs get
this: darcs get --tag 2.2.6
Uploaded by NilsAndersDanielsson at 2009-12-23T15:42:38Z
Distributions Arch:, Debian:2.6.1, Fedora:, FreeBSD:, LTSHaskell:, NixOS:, Stackage:2.6.3
Reverse Dependencies 8 direct, 1 indirect [details]
Executables agda-mode
Downloads 55159 total (557 in the last 30 days)
Rating 2.75 (votes: 8) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]

Readme for Agda-2.2.6

[back to package description]
Agda 2

Table of contents:

* Installing Agda
* Configuring the Emacs mode
* Prerequisites
* Installing a suitable version of Emacs under Windows
* Installation script for (at least) Ubuntu

Installing Agda

There are several ways to install Agda. (Note that this README only
discusses installation of Agda, not its standard library. See the Agda
Wiki for information about the library.)

* Using a binary package, prepared for your platform.

  Recommended if such a package exists. See the Agda Wiki.

* Using stable packages available from Hackage.

  Install the prerequisites mentioned below, then run the following

    cabal install Agda-executable
    agda-mode setup

  The second command tries to set up Emacs for use with Agda. As an
  alternative you can copy the following text to your .emacs file:

    (load-file (let ((coding-system-for-read 'utf-8))
                    (shell-command-to-string "agda-mode locate")))

* Using the source tar balls available from the Agda Wiki, or the
  development version of the code available from our darcs repository.

  1)  Install the prerequisites mentioned below.

  2a) If your system is Unix-like you can now hopefully install the
      Agda 2 library, batch-mode tool and Emacs mode by running the
      following command:

        make install

      If this does not work on your system, or you want to have more
      control, you can follow 2b instead.

  2b) Run the following commands in the top-level directory of the
      Agda source tree:

        cabal install
        agda-mode setup
        cd src/main
        cabal clean       # To ensure recompilation when upgrading.
        cabal install

      The second command tries to set up Emacs for use with Agda. As
      an alternative you can copy the following text to your .emacs

        (load-file (let ((coding-system-for-read 'utf-8))
                        (shell-command-to-string "agda-mode locate")))

      If you want to have more control over where files are installed
      then you can give various flags to cabal install, see
      cabal install --help.

  A section below lists an installation script which should work under
  the Ubuntu distribution of GNU/Linux, assuming that your
  configuration is reasonably standard.

Configuring the Emacs mode

If you want to you can customise the Emacs mode. Just start Emacs and
type the following:

   M-x load-library RET agda2-mode RET
   M-x customize-group RET agda2 RET

This is useful if you want to change the Agda search path, in which
case you should change the agda2-include-dirs variable.

If you want some specific settings for the Emacs mode you can add them
to agda2-mode-hook. For instance, if you do not want to use the Agda
input method (for writing various symbols like ∀≥ℕ→π⟦⟧) you can add
the following to your .emacs:

(add-hook 'agda2-mode-hook
          '(lambda ()
             ; If you do not want to use any input method:
             ; If you want to use the X input method:
             (set-input-method "X")

Note that, on some systems, the Emacs mode changes the default font of
the current frame in order to enable many Unicode symbols to be
displayed. This only works if the right fonts are available, though.
If you want to turn off this feature, then you should customise the
agda2-fontset-name variable.


You need recent versions of the following programs/libraries:

   GNU Emacs:

You should also make sure that programs installed by cabal-install are
on your shell's search path.

For instructions on installing a suitable version of Emacs under
Windows, see below.

Non-Windows users need to ensure that the development files for the C
library zlib are installed (see Your package manager
may be able to install these files for you. For instance, on Debian or
Ubuntu it should suffice to run

  apt-get install zlib1g-dev

as root to get the correct files installed.

Installing a suitable version of Emacs under Windows

Note that Agda code often uses mathematical and other symbols
available from the Unicode character set. In order to be able to
display these characters you may want to follow the procedure below
when installing Emacs under Windows.

1. Install NTEmacs 22.

   Download from
   the self-extracting executable

   When executed, it asks where to extract itself.  This can be
   anywhere you like, but here we write the top directory for ntemacs as
   in the following.

   What follows is tested only on this version.  Other versions may
   work but you have to figure out yourself how to use Unicode fonts
   on your version.

2. Install ucs-fonts and mule-fonts for emacs.

   Download from
   the tar file
   Let us write the top directory of extracted files as
   Next we create some derived fonts.
       cd c:/pkg/ucs-fonts/submission
       make all-bdfs
   This gives an error message about missing fonts, but ignore it.

   Download from
   the tar file
   The untarred top directory is named "packages", but we are only
   interested in the subdirectory "packages/fonts".  Let us assume
   we moved this subdirectory to

   Add the following to your .emacs

;;;;;;;;; start of quoted elisp code

(setq bdf-directory-list

(setq w32-bdf-filename-alist
      (w32-find-bdf-fonts bdf-directory-list))

    chinese-gb2312:-ISAS-Fangsong ti-Medium-R-Normal--16-160-72-72-c-160-GB2312.1980-0,
    " t)

(setq font-encoding-alist
      (append '(
                ("JISX0208" (japanese-jisx0208 . 0))
                ("JISX0212" (japanese-jisx0212 . 0))
                ("CNS11643.1992.1-0" (chinese-cns11643-1 . 0))
                ("GB2312" (chinese-gb2312 . 0))
                ("KSC5601" (korean-ksc5601 . 0))
                ("VISCII" (vietnamese-viscii-lower . 0))
                ("MuleArabic-0" (arabic-digit . 0))
                ("MuleArabic-1" (arabic-1-column . 0))
                ("MuleArabic-2" (arabic-2-column . 0))
                ("muleindian-1" (indian-1-column . 0))
                ("muleindian-2" (indian-2-column . 0))
                ("MuleTibetan-0" (tibetan . 0))
                ("MuleTibetan-1" (tibetan-1-column . 0))
                ) font-encoding-alist))

;;;;;;; end of quoted elisp code

   To test the fonts, try

       M-x eval-expression RET
       (set-default-font "fontset-bdf") RET
       M-x view-hello-file

   You should see all the characters without white-boxes.

Installation scripts for Ubuntu 9.10

Installs a released version:

  sudo apt-get install agda-mode agda-bin

Installs the development version:

  sudo apt-get install ghc6 happy alex darcs emacs haskell-mode zlib1g-dev make
  tar xzf cabal-install-0.6.4.tar.gz
  cd cabal-install-0.6.4
  cd ..
  $HOME/.cabal/bin/cabal update
  darcs get --lazy
  cd Agda
  make CABAL_CMD="$HOME/.cabal/bin/cabal" install