[Agda] forall in parameters for data

[Nils Anders Danielsson]

On Tue, Jun 10, 2008 at 3:38 PM, Ulf Norell <ulfn at cs.chalmers.se> wrote:
>
> No, there isn't. The shortest you can get away with is
>
>   data Path {I : _}{O : _}{S : _}{P : _}(Q : ...)

This has annoyed me as well. Could not there be an implicit forall
just after the name of the data type? All arguments in the parameter
list need to be named anyway, so there would be no confusion. And it
would probably take you fifteen minutes to implement.

-- 
/NAD