The standard library aims to contain all the tools needed to write both programs and proofs easily. While we always try and write efficient code, we prioritize ease of proof over type-checking and normalization 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 are several 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.
See the installation instructions for 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 module index for older versions of the library is also available. For example, version 1.7 can be found at https://agda.github.io/agda-stdlib/v1.7/, just replace in the URL 1.7 with the version that you need.
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.
Instructions for updating the experimental branch.
The experimental branch contains non-backward 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 --cubical-compatible flag, which since Agda v2.6.3 supersedes the former --without-K flag. Please consult
GenerateEverything.hs
for a full list of modules that use axiom K, requiring the --with-K flag.
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. For those who would simply like to help out, issues marked with
the low-hanging-fruit tag are a good starting point.