[Agda] Module definition order

[Lennart Augustsson]

Could someone explain the rationale for the scoping rules in a module?

It seems that the scope of a definition is from the point it is
defined to the end of the module (except for mutual).  This is like a
throwback to C, except it's worse.  At least in C I can make forward
declarations, and then place my definition where ever I like.

It's very easy to allow definitions in any order (and no mutual
keyword), so why not do that?  Just build the dependency graph and
find the strongly connected components, and that's it.

  -- Lennart