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

[Andreas Abel]

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/