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

[Nils Anders Danielsson]

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"? 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.)


   open import M args as M′ using/hiding/renaming

     ⇒

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

-- 
/NAD