The Agda standard library
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. You can browse the library source code in glorious clickable html here.
Quick installation instructions
Use version v0.17 of the standard library with Agda 184.108.40.206.
Install it as follows. Say you are in directory
$HERE (replace appropriately).
git clone https://github.com/agda/agda-stdlib.git cd agda-stdlib git checkout v0.17 cabal install
The last comment is optional, omit it if you are lacking cabal.
Register it by adding the following line to
To use the standard library in you project
$PROJECT, put a file
$PROJECT.agda-lib file in the project root containing:
depend: standard-library include: $DIRS
$DIRS is a list of directories where Agda
searches for modules, for instance
. (just the project root).
If you want to refer to the standard library in all your
projects, add the following line to
Find the full story at readthedocs.
Contributing to the library
If you would like to suggest improvements, feel free to use the
If you would like to make improvements yourself, follow the instructions in
Non-standard versions of Agda
If you're using an old version of Agda, you can download the corresponding version of the standard library on the Agda wiki.
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
experimental branch contains non-backwards compatible patches for upcoming
changes to the language.
Type-checking with the
After the next full release of Agda, most of the library will be able to
be type-checked with the
--safe flag. Only the following modules are
Data.Char.Unsafe Data.Float.Unsafe Data.Nat.Unsafe Data.Nat.DivMod.Unsafe Data.String.Unsafe Data.Word.Unsafe Debug.Trace IO IO.Primitives Reflection Relation.Binary.PropositionalEquality.TrustMe