[Agda] keywords, syntax

[Wojciech Jedynak]

Hello,

2011/11/14 Ramana Kumar <rk436 at cam.ac.uk>:
> Is there a list of Agda keywords somewhere?
> Or even better, a formal description of the syntax?
> How can I find out about all the different variations on, say, "open"
> (e.g. things like "using", "renaming", "import", etc.) and what
> they're supposed to do?

The best reference I found so far is Ulf Norell's PhD dissertation
(see chapter 5.):
http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf

It a little dated though. For the most up to date information on
syntax you can browse the code for the parser in Agda's source code.

The manual on Agda wiki has some useful information, but it's rather
incomplete. The chapter on modules seems OK, though.
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.TOC

Greetings,
W. Jedynak