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

[Ulf Norell]

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 Γ Δ

/ Ulf


On Thu, Feb 4, 2016 at 6:48 PM, Andreas Abel <andreas.abel at ifi.lmu.de>
wrote:

> On 04.02.2016 17:43, Nils Anders Danielsson wrote:
>
>> On 2016-02-04 17:19, Andreas Abel wrote:
>>
>>> Hi, this is a poll about what you would expect Agda to do about the
>>> hiding of parameters if you have definitions inside a parametrized
>>> record inside a parametrized module.
>>>
>>
>> I suspect that you're not quite satisfied with the current situation.
>> Let me see if I can guess what you're most annoyed with. Is it the fact
>> that fields and record module definitions are (sometimes) treated
>> differently?
>>
>
> No, frankly, I want to fix a bug, but I do not know the intended semantics.
>
>
> --
> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160205/444e094e/attachment-0001.html