Adding vectors elementwise

Stream: new members

[Martin C. Martin]

I'm defining a type for vector of length n, and a function to add them element wise. I've taken it mostly from section 8.7 in TPIL. However, I get an error I don't understand.

type mismatch at application
  myadd (2::3::nil)
term
  2::3::nil
has type
  vector ?m_1 1.succ : Type ?
but is expected to have type
  Type ? : Type (?+1)

what am I doing wrong?

import algebra.field.basic

universe u
inductive vector (α : Type u) : ℕ → Type u
| nil {}                              : vector 0
| cons {n : ℕ} (a : α) (v : vector n) : vector (nat.succ n)

namespace vector
local notation (name := cons) h :: t := cons h t

variables (F : Type*) [field F]

def myadd : Π { n : ℕ }, (vector F n) → (vector F n) → (vector F n)
| .(0)     nil           nil         := nil
| .(n + 1) (@cons .(F) n a₁ v₁) (cons a₂ v₂) := cons (a₁ + a₂) (myadd v₁ v₂)

example : myadd (2 :: 3 :: nil) (5 :: 7 :: nil) = 7 :: 10 :: nil := sorry

end vector

[Ruben Van de Velde]

First explicit argument to myadd is F, not a vector

[Martin C. Martin]

Oh, I thought it would be implicit since it's a variable imported from the context. Is there a good description somewhere for what things are implicit or explicit? Or the def syntax?

[Ruben Van de Velde]

(F) is explicit, {F} is implicit (and [field F] is another kind of implicit)

[Martin C. Martin]

Ah, in the variables statement! Thanks.

[Martin C. Martin]

So now I've ditched the Field altogether, since ℕ isn't a field, and have defined myadd as:

variable {α : Type u}
def myadd [has_add α] : Π { n : ℕ}, (vector α n) → (vector α n) → (vector α n)

However, when I try to enable infix + notation like this:

variable {n : ℕ}
instance : has_add (vector α n) := ⟨myadd⟩

It fails because I'm not restricting it only to places where α has has_add α . How do I do that?

[Eric Wieser]

instance [has_add α] : has_add (vector α n) := ⟨myadd⟩