The Iowa Agda Library (IAL)
Aaron Stump

1. About the library

The goal is to provide a concrete library focused on verification
examples, as opposed to mathematics.  The library has a good number
of theorems for booleans, natural numbers, and lists.  It also has
trees, tries, vectors, and rudimentary IO.  A number of good ideas
come from Agda's standard library.

2. Using the library 

This library has been tested with Agda 2.5.4.  If you are
using an older version of Agda, try version 1.2:

https://svn.divms.uiowa.edu/repos/clc/projects/agda/ial-releases/1.2

Starting with Agda 2.5.1, to use the library you must add it to your
Agda libraries.  On linux, create the directory ~/.agda, and add a file
called "libraries" to it, containing the full path to the .agda-lib file
contained in this directory (for the IAL version 1.3).  Then create
a file called "defaults", and add the word "ial" to it (no quotes).
These steps tell Agda where the IAL library is, and that you want to
include it when opening .agda files in emacs (or with the command-line
tool).

In Agda, you can include the whole library by importing lib.agda.  

You can compile the whole library by running "make".

The library is set up so there are no name conflicts between modules
(except sometimes I have several versions of the same module, like
nat-division and nat-division-wf, and there might
be name conflicts in such cases).

3. Browsing the library

You can get some overview of what is in the library by following
imports from lib.agda (this is the main entry point for the library).

4. Credits

The library is mostly written by myself, but it also includes some
contributions from John Bodeen, Harley Eades, and undergraduates who
took my Programming Language Concepts class, Spring 2014 and 2015,
especially Tom Werner.

5. Releases

Recent releases of the IAL can be found here:

https://github.com/cedille/ial/releases

Older released versions of the library can be found at

https://svn.divms.uiowa.edu/repos/clc/projects/agda/ial-releases

The development version is at

https://github.com/cedille/ial

6. License

This library is currently provided under the MIT License, see LICENSE.txt.

7. Documentation

There is no formal documentation currently, besides comments in the files.

Much of the library is described in my book, "Verified Functional
Programming in Agda", published 2016 with ACM Books.