[Agda] keywords, syntax

[Ramana Kumar]

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?
Similarly it would be nice to see an exhaustive overview of the kinds
of statements or expressions that might appear in a source file.
So far I see: value type declarations, value definitions, datatype
definitions, record definitions, various assorted directives to do
with scoping and modules, ....