[Agda] Problem with reversing vector

Lyndon Maydwell maydwell at gmail.com
Fri Jun 15 11:21:16 CEST 2012

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:

.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!

More information about the Agda mailing list