Agda: Excluding some files of a library

[ice1000]

Like, I wanted to generate html from my codes, so I definitely want to write a file named index.agda (which will generate index.html, the homepage), which conflicts with the stdlib's one.

If I can exclude the stdlib's index.agda that'll be awesome.

Mentioned in #2847

[fredefox]

I just wanted to repeat my comment from #2847:

This issue also occurs in Haskell and there it can be solved with the language extension Package-qualified imports.

[nad]

I have used README modules in several projects, but I avoid "exporting" such modules, because that would lead to name clashes. Perhaps the standard library does not need to expose a module called index.agda.

[UlfNorell]

This won't happen for the current library system, which is nothing more than a dressed-up way of managing include paths.