[Agda] Duplicate parameter names in type definition

[Ulf Norell]

On Thu, Oct 29, 2009 at 7:51 PM, Vag Vagoff <vag.vagoff at gmail.com> wrote:

> module Bug where
>
> data Type : Set where value : Type
> data Test (h : Type) (h : Type) : Set where -- duplicate names [!]
>    tst : Test _ _
> test : Test value value
> test = tst
>
> This source typechecks. Is it intended compiler behaviour?
>

That's how it works at the moment. There's a discussion on shadowing in this
issue on the bug tracker:

http://code.google.com/p/agda/issues/detail?id=30

Feel free to add comments to it.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091030/3024faa6/attachment.html