The standard library aims to contain all the tools needed to easily write both programs and proofs. While we always try and write efficient code, we prioritise ease of proof over type-checking and normalisation performance. If computational performance is important to you, then perhaps try agda-prelude instead.
If you're looking to find your way around the library, there's various different ways to get started:
-
The library's structure and the associated design choices are described in the README.agda.
-
The README folder, which mirrors the structure of the main library, contains examples of how to use some of the more common modules. Feel free to open a new issue if there's a particular module you feel could do with some more documentation.
-
You can browse the library's source code in glorious clickable html here.
-
Finally you can get an overview of the entire library by looking at the index which lists every module it contains (minus any deprecated modules).
See the instructions here for how to install the latest version of the standard library.
If you're using an old version of Agda, you can download the corresponding version of the standard library on the Agda wiki. The index for older versions of the library can be found at, for example, https://agda.github.io/agda-stdlib/v0.17/ where 0.17 can be replaced as required.
If you're using a development version of Agda rather than the latest official release
you should use the experimental branch of the standard library rather than master.
The experimental branch contains non-backwards compatible patches for upcoming
changes to the language.
Most of the library can be type-checked using the --safe flag. Please consult
GenerateEverything.hs
for a full list of modules that use unsafe features.
Most of the library can be type-checked using the --without-k flag. Please consult
GenerateEverything.hs
for a full list of modules that use axiom K.
If you would like to suggest improvements, feel free to use the Issues tab.
Even better if you would like to make the improvements yourself, we have instructions
in HACKING to help
you get started.