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

Andreas Abel andreas.abel at ifi.lmu.de
Thu Oct 18 17:04:10 CEST 2012

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


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

More information about the Agda mailing list