[Agda] Re: Replacement of 'as' in module statements?

[Andreas Abel]

On 18.10.12 5:54 PM, Nils Anders Danielsson wrote:
> On 2012-10-18 17:04, Andreas Abel wrote:
>> Maybe then I should enable the syntax
>>
>>    open import M args as M'
>>
>> since I now understand how to implement it:
>>
>>    import M as .Fresh
>>    module M' = .Fresh args
>
> Did you forget "private"?

Yes.

 > I suggest the following translations:
>
>    open import M args using/hiding/renaming
>
>      ⇒
>
>    import M as .Fresh
>    private
>      open module M = .Fresh args using/hiding/renaming
>
>      (One cannot write "open module M = ..." if M is a qualified module
>      name, but I think it's still clear what the intention of the code
>      above is.)

Naa, here I disagree.  M by itself should not be brought into scope 
because then you cannot do a

   open import M

later.

>    open import M args as M′ using/hiding/renaming
>
>      ⇒
>
>    import M as .Fresh
>    private
>      open module M′ = .Fresh args using/hiding/renaming

Agreed & implemented.

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/