[Agda] general question

[Martin Escardo]

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?

Martin

On 03/05/11 10:59, Dominique Devriese wrote:
> Martin,
>
> 2011/5/3 Martin Escardo<m.escardo at cs.bham.ac.uk>:
>> Suppose I define dependent vectors as follows
>>
>> data Vec (A : ℕ → Set) : ℕ → Set where
>>   [] : Vec A O
>>   _::_ : {n : ℕ} → A n → Vec A n → Vec A (succ n)
>>
>> In some cases I want to swap the order of A and n when I write Vec A n,
>> writing instead Vec 0 A because occasionally I want to omit A. I don't
>> understand well enough the general syntax of "data" to be able to do that.
>> Any ideas?
>
> I guess you could just define
>
>    open import Function using (flip)
>
>    Vec' : ℕ → (ℕ → Set) → Set
>    Vec' = flip Vec
>
> Or is that not what you want?
>
> Dominique
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda