Standard Library


For versions 0.7 and earlier, the READMEs contain and link to library documentation.

Development version

Note that the development version of the library often requires the development version of Agda.

  • Git repository. README.
  • You can get the development version as follows:
    git clone

Contributions are welcome, see the README.

From Agda-2.5: Telling Agda about the location of the standard library


Until Agda-2.4: Setting up the Emacs mode for use with the library

  • Download the library and unpack it into some directory DIR.
  • In Emacs, type the following commands:
   M-x load-library RET agda2-mode RET
   M-x customize-group RET agda2 RET
  • Look for the option Agda2 Include Dirs. Insert the path DIR/src.
  • In the development version under git one needs instead to look for the option Agda2 Program Args. Insert for each path element —include-path=path where path is your path. One path element should be the current directory, ., and one should be the location of the standard-library DIR/src.
  • Click Save for Future Sessions.
  • If the Save for Future Sessions is grey, click the State button inside Agda2 Include Dirs and choose Save for Future Sessions there.