adding vectors

Stream: new members

[Iocta]

The exercises say to write add for these vectors. I think the signature is like

def add ( α : Type u) ( n : ℕ ): vec α n -> vec α n -> vec α n

but I don't see how to iterate or extract values from inside.

[Simon Hudon]

Can you show the exercise in question? I don't think it can be formulated in terms of constants like your snippet shows

[Iocta]

Number 3 from https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html

[Mario Carneiro]

The exercise is only to write down the type of vec_add, not its definition (which requires details about inductive types that come later in the book)

[Iocta]

Ah. Thanks.