Zulip Chat Archive

Stream: new members

Topic: adding vectors


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Iocta (Dec 15 2019 at 08:58):

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

view this post on Zulip 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)

view this post on Zulip Iocta (Dec 15 2019 at 09:19):

Ah. Thanks.


Last updated: May 10 2021 at 00:31 UTC