[Agda] A quiz: what should the types of these definitions be?

[Ulf Norell]

On Fri, Feb 5, 2016 at 9:13 AM, Andreas Abel <andreas.abel at ifi.lmu.de>
wrote:

> On 05.02.2016 08:34, Ulf Norell wrote:
>
>> Without cheating, I would expect
>>
>>    module M Γ where
>>      record R Δ
>>
>> to yield the same types for functions and projections as
>>
>>    module M where
>>      record R Γ Δ
>>
>
> But this means that inside M, there are declarations that do not have the
> module telescope Gamma as a prefix, but the hiding-modified one.
>
> For instance,
>
>   module M (A : Set) where
>     record R : Set where
>       data D (a : A) : Set where
>     open R public
>     data E (a : A) : Set
>
> then
>
>   E = M.E Nat
>
> is ok while
>
>   D = M.D Nat
>
> will give a type error?
>

Yes.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160205/297615a9/attachment.html