[Agda] forall in parameters for data

[Ulf Norell]

On Tue, Jun 10, 2008 at 4:33 PM, Thorsten Altenkirch <txa at cs.nott.ac.uk>
wrote:

> Hi,
>
> is there any way to use forall when declaring the parameters of a datatype?
> I.e. we would like to write
>
>  data Path forall {I O S P}
>            (Q : (o : O) -> S o -> I -> Set) :
>            (o : O) -> (WI S P o) -> I -> Set where


No, there isn't. The shortest you can get away with is

  data Path {I : _}{O : _}{S : _}{P : _}(Q : ...)

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080610/2c125c82/attachment.html