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

Nils Anders Danielsson nad at chalmers.se
Fri Oct 19 12:01:50 CEST 2012

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′


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


More information about the Agda mailing list