[Agda] general question

[Dominique Devriese]

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