Stream: new members

Iocta (Dec 15 2019 at 06:27):

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 (Dec 15 2019 at 08:32):

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

Mario Carneiro (Dec 15 2019 at 09:07):

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 (Dec 15 2019 at 09:19):

Ah. Thanks.

Last updated: May 10 2021 at 00:31 UTC