[Agda] Examples

[Samuel Bronson]

On 5/18/08, Nils Anders Danielsson <nils.anders.danielsson at gmail.com> wrote:
> On Sat, May 17, 2008 at 9:09 PM, Lennart Augustsson

>  Perhaps one should also take a closer look at the remaining examples.
>  Just because they type check does not mean that they are idiomatic or
>  elegant.

Explanation of what the example is doing and why would also be
welcome. Could be as little as a reference to a paper or as much as
one of Oleg's .lhs files. Pointers to other examples showing
alternative approaches would also be welcome.