matrix.vec_cons and fin.cons

Stream: new members

[Vasily Ilin]

In docs#matrix.vec_cons, we see matrix.vec_cons h t = fin.cons h t. But matrix.vec_cons and fin.cons have different types and behave differently. I understand the type of matrix.vec_cons but not the type of fin.cons. Can anyone explain please?

import data.matrix.notation

variables (n : ℕ) (α : Type) (v : fin n → α) (w : α)
#check matrix.vec_cons w v -- works
#check fin.cons w v -- does not work
#check fin.snoc v w -- does not work

[Vasily Ilin]

What does α 0 mean in the following type? It seems that it's the type of the first element. But then why don't we take the actual first element as input?

fin.cons : Π {n : ℕ} {α : fin (n + 1) → Type u}, α 0 → (Π (i : fin n), α i.succ) → Π (i : fin (n + 1)), α i

[Eric Wieser]

What does α 0 mean in the following type? It seems that it's the type of the first element.

Yes, it does mean that

[Eric Wieser]

The reason that fin.cons w v fails is that lean isn't clever enough to work out what α you meant

[Eric Wieser]

@fin.cons _ (\lam i, α) w v will probably work