[Agda] Problem with reversing vector

[Lyndon Maydwell]

Hi Agda.

I'm trying to figure out how to reverse a vector. Obviously I'm new to
Agda and this problem seems trivial.

So far, I have the following:


data Vec (A : Set) : ℕ → Set where
   ε   : Vec A zero
   _►_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

vconcat : {A : Set} → {m n : ℕ} → Vec A m → Vec A n → Vec A (m + n)
vconcat ε y = y
vconcat (y ► ys) xs = y ►  (vconcat ys xs)

vrev : {A : Set} → {n : ℕ} → Vec A n → Vec A n
vrev ε = ε
vrev (y ► ys) = vconcat (vrev ys) (y ► ε)



This all checks except vrev:

/Users/agda/Code/agda/LYAA/peano.agda:147,17-42
.n + suc zero != suc .n of type ℕ
when checking that the expression vconcat (vrev ys) (y ► ε) has
type Vec .A (suc .n)


Now I would think that ".n + suc zero" does equal "suc .n of type ℕ",
but maybe I need to prove that somehow?

No need to give me an answer, any tips would be greatly appreciated!