Exercise from the lean manual

Stream: new members

[yuppie]

I am trying to solve ex. 2.10.3 from the online tutorial (defining addition on vector nat n). I have tried the following:
def vec_add (n : nat) : vector nat n → vector nat n → vector nat n
| ⟨ [], h ⟩ _ := ⟨ [], h ⟩
| _ ⟨ [], h ⟩ := ⟨ [], h ⟩
| ⟨ a :: v, h ⟩ ⟨ b :: w, g ⟩ := ⟨ (a+b) :: (vec_add ⟨v (congr_arg nat.pred h)⟩ ⟨w congr_arg nat.pred g⟩), h ⟩
#check vec_add
But the las case does not type check. The error message says the following:
function expected at
v
term has type
list ℕ
So somehow I messe up converting v into a vector of length n-1 but I have no idea how to do that.

I am still starting to learn lean. Does anybody have any idea?

[Reid Barton]

You need commas after v and then after w.

[Reid Barton]

Although that still won't work for other reasons.

[yuppie]

Thanks, that was stupid of me. I will try to fix the second argument.