Zulip Chat Archive

Stream: new members

Topic: Exercise from the lean manual


view this post on Zulip yuppie (Oct 28 2019 at 20:07):

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?

view this post on Zulip Reid Barton (Oct 28 2019 at 20:26):

You need commas after v and then after w.

view this post on Zulip Reid Barton (Oct 28 2019 at 20:26):

Although that still won't work for other reasons.

view this post on Zulip yuppie (Oct 29 2019 at 17:32):

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


Last updated: May 11 2021 at 00:31 UTC