[Agda] modules named `_`

[David Darais]

I agree that the semantics are useful, and therefore deserve an economical syntax. My comment is about the semantics of the current syntax being unexpected (which perhaps you also disagree with).

What about:

open module (A : Set) where
  foo : A → A
  foo x = x

?

> On Sep 25, 2015, at 3:22 PM, effectfully <effectfully at gmail.com> wrote:
> 
> 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