Standard Library


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.

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.