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

[Nils Anders Danielsson]

On 2012-10-19 02:06, Andreas Abel wrote:
> Naa, here I disagree.  M by itself should not be brought into scope
> because then you cannot do a
>
>    open import M
>
> later.

I realised that I can write

   open import M args as M,

so I drop my suggestion.

The following syntax seems to be missing:

   import M args as M′

Semantics:

   import M as .Fresh
   private
     module M′ = .Fresh args

-- 
/NAD