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

[Nils Anders Danielsson]

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?

-- 
/NAD