[Agda] modules named `_`

[effectfully]

Hi.

To me `module _ ... where' has perfect semantics. I'm using this
construction all the time (e.g. it's used five times only in this [1]
module). And also writing "open public" every time would be annoying.

If you want a nameless closed module (i.e. there is no way to bring
stuff from this module to scope) you can explicitly use the `private'
keyword:

module _ (A : Set) where
  private
    foo : A → A
    foo x = x
module _ (A : Set) where
  private
    foo : A → A
    foo x = x

[1] https://github.com/effectfully/Categories/blob/master/Category/Category.agda