[Agda] general question

[Dominique Devriese]

Martin,

2011/5/3 Martin Escardo <m.escardo at cs.bham.ac.uk>:
> Dominuqe, thanks. Yes, I can do this.
>
> But what is, in the syntax of the data declaration, forcing me to have A
> first? And why?

I guess this is related to the distinction between data type indices
and parameters in Agda data definitions. I don't immediately find a
good reference, but other people on this list will be able to explain
this, I think.

Dominique