Zulip Chat Archive

Stream: new members

Topic: adding vectors

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

Iocta (Dec 15 2019 at 08:58):

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

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: Dec 20 2023 at 11:08 UTC