[Agda] Module definition order

[Nils Anders Danielsson]

On Thu, May 22, 2008 at 9:51 AM, Ulf Norell <ulfn at cs.chalmers.se> wrote:
>
> That's a good point. A reasonable thing to do would be to force the
> programmer to specify the strongly connected components, but allow them to
> appear in any order.

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.

-- 
/NAD