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

[Andreas Abel]

On 18.10.2012 14:55, Nils Anders Danielsson wrote:
> On 2012-10-18 10:17, Andreas Abel wrote:
> Yes, IMO that's not so nice.
>
>> The current
>>
>>    import MP as M
>>    open import MP as M
>>
>> could be deprecated in favor of
>>
>>    module M = import MP
>>    open M = import MP
>
> These don't mean the same thing: "import MP as M" doesn't create any new
> modules, whereas "module M = import MP" introduces a new, exported
> module M. One could use
>
>    private
>      module M = import MP,
>
> but that's rather bulky.

Aha, so I need to understand 'as' as '=' + private.

Mmh, then the story is not so smooth.

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

Cheers,
Andreas

-- 
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/