Convention for import statement ordering

[fredrik-bakke]

Jonathan and I have been working together to try to define a ruleset for how import statements should be ordered, as he is developing a script to automate the sorting of these (#488 #487 #484).

The import order that we are currently proposing is the following.

1. public import statements
2. non-public Agda primitive imports
3. non-public import statements from the same namespace
4. non-public import statements from other namespaces
5. other open statements (this seems to be unconventional, but alas there are instances of this in the library)

Within these categories, the statements should be sorted alphabetically.

The reasoning is that this will hopefully correlate well with the relevance of each individual import, while still being somewhat intuitive to the user/contributor.

[fredrik-bakke]

Alright, after speaking with Egbert, the new proposal is as follows:

1. public import statements
2. non-public import statements
3. other open statements (although these should not occur)

Within each category, the statements are sorted alphabetically, and each namespace is separated with an empty line.

[EgbertRijke]

I was just about to write the same:)

These seem very sensible conventions to me.

[fredrik-bakke]

As an addendum, import statements are sorted by namespaces first, not just alphabetically as a whole. (#497)

In practice, this means foundation imports come before foundation-core imports, even though the string foundation-core. comes before foundation. alphabetically.