[Agda] Renaming of a module, associated with a record, doesn't hide the original name.

[Andreas Abel]

This behavior is due to the fact that you can qualify definitions in 
records both by their module name and their record type name.  If you 
change the record R to a plain module, you will not get the described 
behavior.  (Similar for data constructors.)

Cheers,
Andreas

On 31.07.2015 03:35, effectfully wrote:
> Hi.
>
>      module _ where
>
>      open import Data.Nat
>
>      module M where
>        record R : Set where
>          z = 0
>      open M renaming (module R to R')
>
>     test = {!!}
>
> In `test' both `R.z' and `R'.z'are in scope.
>
> If I write
>
>      open M renaming (module R to R'; R to R')
>
> instead, then `R.z' is not in scope in `test'.
>
> If I write
>
>      open M renaming (R to R')
>
> then both `R.z' and `R'.z' are in scope again.
>
> I guess in the first and the third cases there should be in scope only
> `R'.z' and `R.z' accordingly. Is the current behaviour a bug or am I
> misunderstanding something?


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/