[Agda] Private anonymous modules

[Favonia]

Hi all,

I'd like to initiate the discussion about anonymous modules (modules with
names '_') under the keyword 'private'. Currently, such a module will be
opened publicly, effectively ignoring the private keyword. I wonder how
people feel about alternatives like having anonymous modules under
'private' stay private, changing the semantics of 'open public' under
'private', or even banning public opening under 'private' but giving
anonymous modules special treatments. Personally I am in favor of the last
option.

I opened an issue on GitHub this morning
https://github.com/agda/agda/issues/2199 and Andreas Abel quickly patched
Agda to at least give you an error message. There is a small discussion on
GitHub among Andreas, Ulf and me but Andreas (and me too) thinks we should
discuss this in a larger forum.

Best,
Favonia
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160920/398c2b16/attachment.html