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 like 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 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.

[Skip to Readme]
Versions [RSS] [faq] 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 (info)
Dependencies array (>=0.1 && <1), base (==3.*), binary (>=0.4.4 && <0.5), bytestring (>= && <1), containers (>=0.1.0 && <1), directory (==1.*), filepath (>=1.1 && <2), ghc-prim (>=0.1 && <1), haskeline (>=0.3 && <0.7), haskell-src (>= && <2), haskell98 (>=1.0.1 && <2), mtl (>=1.1 && <2), old-time (==1.*), pretty (==1.*), process (>= && <2), QuickCheck (==, utf8-string (==0.3.*), xhtml (==3000.2.*), zlib (>= && <1) [details]
License LicenseRef-OtherLicense
Author Ulf Norell, Catarina Coquand, Makoto Takeyama, Nils Anders Danielsson, Andreas Abel, ...
Maintainer Ulf Norell <>
Category Dependent types
Home page
Bug tracker
Uploaded by NilsAndersDanielsson at 2009-03-17T17:46:13Z
Distributions Arch:, Debian:, Fedora:2.6.1, FreeBSD:, LTSHaskell:, NixOS:
Downloads 45701 total (794 in the last 30 days)
Rating 2.75 (votes: 8) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs not available [build log]
All reported builds failed as of 2017-01-02 [all 6 reports]


  • Agda
    • Compiler
      • Agate
        • Agda.Compiler.Agate.Classify
        • Agda.Compiler.Agate.Common
        • Agda.Compiler.Agate.Main
        • Agda.Compiler.Agate.OptimizedPrinter
        • Agda.Compiler.Agate.TranslateName
        • Agda.Compiler.Agate.UntypedPrinter
      • Alonzo
        • Agda.Compiler.Alonzo.Haskell
        • Agda.Compiler.Alonzo.Main
        • Agda.Compiler.Alonzo.Names
        • Agda.Compiler.Alonzo.PatternMonad
      • Agda.Compiler.HaskellTypes
      • MAlonzo
        • Agda.Compiler.MAlonzo.Compiler
        • Agda.Compiler.MAlonzo.Encode
        • Agda.Compiler.MAlonzo.Misc
        • Agda.Compiler.MAlonzo.Pretty
        • Agda.Compiler.MAlonzo.Primitives
    • Interaction
      • Agda.Interaction.BasicOps
      • CommandLine
        • Agda.Interaction.CommandLine.CommandLine
      • Agda.Interaction.Exceptions
      • Agda.Interaction.GhciTop
      • Highlighting
        • Agda.Interaction.Highlighting.Emacs
        • Agda.Interaction.Highlighting.Generate
        • Agda.Interaction.Highlighting.HTML
        • Agda.Interaction.Highlighting.Precise
        • Agda.Interaction.Highlighting.Range
        • Agda.Interaction.Highlighting.Vim
      • Agda.Interaction.Imports
      • Agda.Interaction.MakeCase
      • Agda.Interaction.Monad
      • Agda.Interaction.Options
    • Agda.Main
    • Syntax
      • Agda.Syntax.Abstract
        • Agda.Syntax.Abstract.Name
        • Agda.Syntax.Abstract.Pretty
        • Agda.Syntax.Abstract.Views
      • Agda.Syntax.Common
      • Agda.Syntax.Concrete
        • Agda.Syntax.Concrete.Definitions
        • Agda.Syntax.Concrete.Name
        • Agda.Syntax.Concrete.Operators
          • Agda.Syntax.Concrete.Operators.Parser
        • Agda.Syntax.Concrete.Pretty
      • Agda.Syntax.Fixity
      • Agda.Syntax.Info
      • Agda.Syntax.Internal
        • Agda.Syntax.Internal.Generic
        • Agda.Syntax.Internal.Pattern
      • Agda.Syntax.Literal
      • Agda.Syntax.Parser
        • Agda.Syntax.Parser.Alex
        • Agda.Syntax.Parser.Comments
        • Agda.Syntax.Parser.Layout
        • Agda.Syntax.Parser.LexActions
        • Agda.Syntax.Parser.Lexer
        • Agda.Syntax.Parser.LookAhead
        • Agda.Syntax.Parser.Monad
        • Agda.Syntax.Parser.Parser
        • Agda.Syntax.Parser.StringLiterals
        • Agda.Syntax.Parser.Tokens
      • Agda.Syntax.Position
      • Scope
        • Agda.Syntax.Scope.Base
        • Agda.Syntax.Scope.Monad
      • Agda.Syntax.Strict
      • Translation
        • Agda.Syntax.Translation.AbstractToConcrete
        • Agda.Syntax.Translation.ConcreteToAbstract
        • Agda.Syntax.Translation.InternalToAbstract
    • Termination
      • Agda.Termination.CallGraph
      • Agda.Termination.Lexicographic
      • Agda.Termination.Matrix
      • Agda.Termination.Semiring
      • Agda.Termination.TermCheck
      • Agda.Termination.Termination
    • Agda.Tests
    • Agda.TypeChecker
    • TypeChecking
      • Agda.TypeChecking.Abstract
      • Agda.TypeChecking.Constraints
      • Agda.TypeChecking.Conversion
      • Agda.TypeChecking.Coverage
        • Agda.TypeChecking.Coverage.Match
      • Agda.TypeChecking.DisplayForm
      • Agda.TypeChecking.Empty
      • Agda.TypeChecking.Errors
      • Agda.TypeChecking.EtaContract
      • Agda.TypeChecking.Free
      • Agda.TypeChecking.Implicit
      • Agda.TypeChecking.Injectivity
      • Agda.TypeChecking.MetaVars
      • Agda.TypeChecking.Monad
        • Agda.TypeChecking.Monad.Base
        • Agda.TypeChecking.Monad.Builtin
        • Agda.TypeChecking.Monad.Closure
        • Agda.TypeChecking.Monad.Constraints
        • Agda.TypeChecking.Monad.Context
        • Agda.TypeChecking.Monad.Debug
        • Agda.TypeChecking.Monad.Env
        • Agda.TypeChecking.Monad.Exception
        • Agda.TypeChecking.Monad.Imports
        • Agda.TypeChecking.Monad.MetaVars
        • Agda.TypeChecking.Monad.Mutual
        • Agda.TypeChecking.Monad.Open
        • Agda.TypeChecking.Monad.Options
        • Agda.TypeChecking.Monad.Signature
        • Agda.TypeChecking.Monad.SizedTypes
        • Agda.TypeChecking.Monad.State
        • Agda.TypeChecking.Monad.Statistics
        • Agda.TypeChecking.Monad.Trace
      • Patterns
        • Agda.TypeChecking.Patterns.Match
      • Agda.TypeChecking.Polarity
      • Agda.TypeChecking.Positivity
      • Agda.TypeChecking.Pretty
      • Agda.TypeChecking.Primitive
      • Agda.TypeChecking.Rebind
      • Agda.TypeChecking.Records
      • Agda.TypeChecking.Reduce
      • Rules
        • Agda.TypeChecking.Rules.Builtin
        • Agda.TypeChecking.Rules.Data
        • Agda.TypeChecking.Rules.Decl
        • Agda.TypeChecking.Rules.Def
        • Agda.TypeChecking.Rules.LHS
          • Agda.TypeChecking.Rules.LHS.Implicit
          • Agda.TypeChecking.Rules.LHS.Instantiate
          • Agda.TypeChecking.Rules.LHS.Problem
          • Agda.TypeChecking.Rules.LHS.Split
          • Agda.TypeChecking.Rules.LHS.Unify
        • Agda.TypeChecking.Rules.Record
        • Agda.TypeChecking.Rules.Term
      • Agda.TypeChecking.Serialise
      • Agda.TypeChecking.SizedTypes
      • Agda.TypeChecking.Substitute
      • Agda.TypeChecking.Telescope
      • Test
        • Agda.TypeChecking.Test.Generators
      • Agda.TypeChecking.Tests
      • Agda.TypeChecking.With
    • Utils
      • Agda.Utils.Char
      • Agda.Utils.Either
      • Agda.Utils.FileName
      • Agda.Utils.Fresh
      • Agda.Utils.Function
      • Agda.Utils.Generics
      • Agda.Utils.Graph
      • Agda.Utils.Hash
      • Agda.Utils.IO
      • Agda.Utils.Impossible
      • Agda.Utils.List
      • Agda.Utils.Map
      • Agda.Utils.Maybe
      • Agda.Utils.Monad
        • Agda.Utils.Monad.Undo
      • Agda.Utils.Permutation
      • Agda.Utils.Pointer
      • Agda.Utils.Pretty
      • Agda.Utils.QuickCheck
      • Agda.Utils.ReadP
      • Agda.Utils.SemiRing
      • Agda.Utils.Serialise
      • Agda.Utils.Size
      • Agda.Utils.String
      • Agda.Utils.Suffix
      • Agda.Utils.TestHelpers
      • Agda.Utils.Trace
      • Agda.Utils.Trie
      • Agda.Utils.Tuple
      • Agda.Utils.Unicode
      • Agda.Utils.Warshall
    • Agda.Version


Maintainer's Corner

For package maintainers and hackage trustees


Readme for Agda-2.2.0

[back to package description]

We recommend that you install Agda 2 using a binary package. To
install Agda 2 from source, proceed as follows:

(An appendix below lists a partial installation script for Ubuntu

0) Install prerequisites (recent versions of GHC, Alex, Happy and
   cabal-install, and perhaps also darcs, Emacs and haskell-mode).

   GNU Emacs:
   haskell-mode: (version 2.1 or later)

   Note: If you are downloading a source tar-ball, then you do not
   need Alex, Happy or darcs.

   For non-Windows users:
     The development files for the C library zlib have to be 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.

1) Download Agda 2, perhaps as follows:

     darcs get --partial
     cd Agda

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

     make install PREFIX=<installation location>

   (the PREFIX=<...> part can be omitted if the default location is OK
   for you).

   If your system is not sufficiently Unix-like, or you want to have
   more control, continue reading below.

3) Build and install the Agda 2 library. If you want to install it in
   the default location (you may need root privileges for this), use
   the following command in the root of the Agda source tree:

     cabal install

   You can select another location for the installation of the library
   by using the following command:

     cabal install --prefix=<the install path>

   You can also give other options to the installer, see the built-in
   documentation of cabal-install:

     cabal install --help

4) If you want to use the Emacs mode (recommended), build and install
   it (see below).

5) If you want to use the batch-mode Agda tool (not necessary), go to
   the src/main directory and run the following commands:

     cabal clean    # To ensure recompilation when upgrading.
     cabal install

   (You can give options to cabal-install just as under step 2.)

   When upgrading Agda, note that the batch-mode tool also needs to be

To use the Agda 2 Emacs mode:

-1. Install Emacs.

   (For non-Windows - jump down to **END OF "Under Windows ...")
   **Under Windows you may want to follow the following procedure:

      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.
  **END OF "Under Windows ..."

1. Install Agda 2. (See above.)

2. Copy the .el files in src/emacs-mode to some directory
   <agda-mode-dir>. Example installation:

   mkdir <agda-mode-dir>
   cp src/emacs-mode/*.el <agda-mode-dir>

3. Add the following to your .emacs:

   (add-to-list 'load-path "<agda-mode-dir>")
   (require 'agda2)

   If you have already set up the suffix .agda for use with some other
   mode you may need to remove or alter that setting. You are
   encouraged to use the suffix .alfa for Agda 1 files.

   Now, if you open a file named XXX.agda the buffer will use
   agda2-mode. It may take 5 or 10 seconds before you see anything in
   the buffer, but that is normal.

4. If you want to you can customise some settings. 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.

5. 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")

   A side note: In order to display Unicode characters you need to use
   a font which contains the glyphs in question. If such a font is not
   enabled by default (empty boxes are displayed instead of proper
   characters) you need to select another font. Do this by running
     M-x customize-face RET agda2-fontset-spec RET
   in Emacs (after you have started the Agda mode) and change the
   setting to a suitable font.

Appendix: Partial installation script for (at least) Ubuntu Linux

sudo apt-get install ghc6 happy alex darcs emacs haskell-mode zlib1g-dev
tar xzf cabal-install-0.6.0.tar.gz
cd cabal-install-0.6.0
cd ..
darcs get --partial
cd Agda
sudo make install