[Agda] Module definition order

[Samuel Bronson]

Oops, sent to just Nils the first time for some reason...

> Something like this would also make "literate Agda" more useful. In
> literate programming systems you can usually reorder code chunks in
> some way, so that the resulting code and the resulting document can be
> quite different. I have rarely (never?) felt this need with literate
> Haskell, since I can usually reorder the definitions in the source
> language, but with (the current) Agda the need comes back.

Too bad we are already using all of the symbols that could be used to
make this pretty :-(