Vectors as indexed inductive types

There are two common ways to define vectors in Lean, as indexed inductive types or as structures. In Lean, Vectors are defined as structures. Here, we define vectors as indexed inductive types.

inductive Vec (α : Type u) : ℕ → Type u

• nil {α : Type u} : Vec α 0
• cons {α : Type u} {n : ℕ} (a : α) (v : Vec α n) : Vec α (n + 1)

def Vec.add {α : Type u_1} [Add α] {n : ℕ} : Vec α n → Vec α n → Vec α n

Equations

• x_3.add x_4 = Vec.nil
• (Vec.cons a as).add (Vec.cons b bs) = Vec.cons (a + b) (as.add bs)