[Agda] Learning from examples

[Shin-Cheng Mu]

Hi,

Having written some simple Agda programs, I am very curious to
learn what Agda can do. I will try to learn from code people have
written, and am browsing through the examples directory and choosing
a place to start.

I would like to know what each of the directories are about.
Here are some directories/files that look interesting. I am
guessing what they are about. Is the following correct?

   AIM4/bag -- an implementation of bags?

   AIM5/Hedberg
   AIM5/yoshiki -- They seem to be two different ways of modelling
                   sets. How are they different?
   AIM5/PolyDep -- What is it?

   AIM6/Cat -- category theory
   AIM6/HelloAgda -- an Agda tutorial
   AIM6/Path -- is it about modal logic?
   AIM6/RegExp -- regular expression matching

   cat -- category theory.

   clowns -- is it a library about datatypes?
             (derivative of datatypes, zippers, etc?)

   Setoid.agda -- What is it?

   Subset.agda -- Representing a subtype by a type and a predicate.
              Is it used anywhere?

   sinatra -- modelling monads?

   tait -- lambda calculus, beta-reduction, and proof of strong
           normalisation?

   Termination -- seems like some sample programs testing
                  termination check of Agda?

sincerely,
Shin