[Agda] general question

[Martin Escardo]

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?

Thanks,
Martin